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.0 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.