Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale Sprachen/PVS/metric_space/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 2 kB

Quelle metric_continuity.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Metric Continuity
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            20/3/07  Initial Version
%------------------------------------------------------------------------------

metric_continuity[T1:TYPE, (IMPORTING metric_def[T1]) d1:metric[T1],
                  T2:TYPE, (IMPORTING metric_def[T2]) d2:metric[T2]]:THEORY

BEGIN

  IMPORTING metric_space[T1,d1],
            metric_space[T2,d2],
            topology@topology_def[T1],
            topology@topology_def[T2],
            topology@topology[T1,metric_induced_topology[T1,d1]],
            topology@topology[T2,metric_induced_topology[T2,d2]],
            topology@hausdorff_convergence[T1,metric_induced_topology[T1,d1]],
            topology@hausdorff_convergence[T2,metric_induced_topology[T2,d2]],
            topology@continuity_def[T1,metric_induced_topology[T1,d1],
                                    T2,metric_induced_topology[T2,d2]],
            topology@continuity[T1,metric_induced_topology[T1,d1],
                                T2,metric_induced_topology[T2,d2]]

  f:             VAR [T1->T2]
  x,x0:          VAR T1
  u:             VAR sequence[T1]
  epsilon,delta: VAR posreal

  metric_continuous_at?(f,x0):bool
     = FORALL epsilon: EXISTS delta: FORALL x:
           member(x,ball(x0,delta)) => member(f(x),ball(f(x0),epsilon))

  metric_continuous?(f):bool = FORALL x: metric_continuous_at?(f,x)

  metric_continuous_at_def: LEMMA
     continuous_at?(f,x0) <=> metric_continuous_at?(f,x0)

  metric_continuous_def: LEMMA
     continuous?(f) <=> metric_continuous?(f)

  metric_continuity_limit: LEMMA
     convergence?(u,x) AND metric_continuous_at?(f,x) =>
     convergence?(f o u, f(x))

  metric_continuous: TYPE = (metric_continuous?)

  metric_continuous_is_continuous:
                            JUDGEMENT metric_continuous SUBTYPE_OF continuous

  continuous_is_metric_continuous:
                            JUDGEMENT continuous SUBTYPE_OF metric_continuous

  uniform_continuous?(f):bool =
     (FORALL epsilon: EXISTS delta: FORALL x,x0:
                  member(x,ball(x0,delta)) => member(f(x),ball(f(x0),epsilon)))

  uniform_continuous: LEMMA uniform_continuous?(f) => continuous?(f)

  uniform_continuous: TYPE = (uniform_continuous?)

  uniform_continuous_is_continuous:
         JUDGEMENT uniform_continuous SUBTYPE_OF continuous

  IMPORTING  finite_sets@finite_sets_minmax[posreal,<=] % proof only

  compact_uniform_continuous: LEMMA
     compact_subset?(metric_induced_topology[T1,d1],fullset[T1]) =>
              (continuous?(f) <=> uniform_continuous?(f))

END metric_continuity

quality93%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.