|
%---------------------------------------------------------------------------------------------------------
%
% Continuity of functions on product (metric) spaces
%
% Author: Anthony Narkawicz, NASA Langley
%
%
% Version 1.0 August 19, 2009
%
%---------------------------------------------------------------------------------------------------------
cross_metric_cont[T1:Type+,d1:[T1,T1->nnreal],
T2:Type+,d2:[T2,T2->nnreal],T3:TYPE+,d3:[T3,T3->nnreal]]: THEORY
BEGIN
ASSUMING IMPORTING metric_spaces
fullset_metric_space1: ASSUMPTION metric_space?[T1,d1](fullset[T1])
fullset_metric_space2: ASSUMPTION metric_space?[T2,d2](fullset[T2])
fullset_metric_space3: ASSUMPTION metric_space?[T3,d3](fullset[T3])
ENDASSUMING
IMPORTING cross_metric_spaces[T1,d1,T2,d2], continuity_ms_def[[T1,T2],d[T1,d1,T2,d2],T3,d3],
uniform_continuity[T1,d1,T3,d3]
S: VAR set[[T1,T2]]
X: VAR set[T1]
Y: VAR set[T2]
f: VAR [[T1,T2] -> T3]
product_cont_equiv: LEMMA
continuous?(f,S) IFF
(FORALL (x: (S), epsilon: posreal): EXISTS (delta: posreal):
FORALL (y: (S)): (d1(x`1,y`1) <= delta AND d2(x`2,y`2) <= delta)
IMPLIES d3(f(x),f(y))<epsilon)
product_cont_product_subset: COROLLARY
continuous?(f,fullset[[(X),(Y)]]) IFF
(FORALL (x: (X), y: (Y), epsilon: posreal): EXISTS (delta: posreal):
FORALL (z: (X), w: (Y)): (d1(x,z) <= delta AND d2(y,w) <= delta)
IMPLIES d3(f(x,y),f(z,w))<epsilon)
% ----------- Uniform Continuity In One Variable ---------------
uniformly_continuous_in_first?(f,X,Y): bool =
FORALL (y1: (Y), epsilon: posreal): EXISTS (delta: posreal):
FORALL (x1,x2: (X), y2: (Y)): (d1(x1,x2) <= delta AND d2(y1,y2) <= delta)
IMPLIES d3(f(x1,y1),f(x2,y2))<epsilon
uniformly_continuous_in_second?(f,X,Y): bool =
FORALL (x1: (X), epsilon: posreal): EXISTS (delta: posreal):
FORALL (x2: (X), y1,y2: (Y)): (d1(x1,x2) <= delta AND d2(y1,y2) <= delta)
IMPLIES d3(f(x1,y1),f(x2,y2))<epsilon
% --------- An Equivalent, Sequence Definition Of Uniform Continuity In One Variable ----
one_variable_unif_cont_sequence: LEMMA NOT uniformly_continuous_in_first?(f,X,Y) IFF
EXISTS (epsilon: posreal): EXISTS (y: (Y)): EXISTS (seq: [posint -> [T1,T1,T2]]):
FORALL (n: posint):
(X(seq(n)`1) AND X(seq(n)`2) AND Y(seq(n)`3)
AND d1(seq(n)`1,seq(n)`2) < 1/n AND d2(y,seq(n)`3) < 1/n
AND d3(f(seq(n)`1,y),f(seq(n)`2,seq(n)`3)) > epsilon)
%--------- This implies that the associated curried function is uniformly continuous ----
curried_is_uniform: LEMMA uniformly_continuous_in_first?(f,X,Y) IMPLIES (FORALL (y: (Y)):
uniformly_continuous?((LAMBDA (t: T1): f(t,y)),X))
END cross_metric_cont
[ Seitenstruktur0.0Drucken
etwas mehr zur Ethik
]
|
