Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: metric_continuity.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.