|
%------------------------------------------------------------------------------
% 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.21 Sekunden
(vorverarbeitet)
¤
|
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.
|
