|
%---------------------------------------------------------------------------------------------------
%
% One-Variable Uniform Continuity of Functions on Product (Metric) Spaces
%
% Author: Anthony Narkawicz, NASA Langley
%
%
% Version 1.0 August 25, 2009
%
%---------------------------------------------------------------------------------------------------
cross_metric_uniform_continuity[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],
cross_metric_cont[T1,d1,T2,d2,T3,d3], compactness[T1,d1]
S: VAR set[[T1,T2]]
X: VAR set[T1]
Y: VAR set[T2]
f: VAR [[T1,T2] -> T3]
multiary_Heine: THEOREM
compact?(X) AND continuous?(f,fullset[[(X),(Y)]])
IMPLIES uniformly_continuous_in_first?(f,X,Y)
multi_Heine_Corollary1: COROLLARY
compact?(X) AND continuous?(f,fullset[[(X),(Y)]])
IMPLIES
FORALL (y1: (Y), epsilon: posreal): EXISTS (delta: posreal):
FORALL (y2: (Y)): (d2(y1,y2) <= delta)
IMPLIES (FORALL (x: (X)): d3(f(x,y1),f(x,y2)) < epsilon)
% A Type Consisting Of All Functions That Are Uniformly Continuous In The First Variable
first_var_unif(X,Y): TYPE = {g: [[T1,T2] -> T3] | uniformly_continuous_in_first?(g,X,Y)}
END cross_metric_uniform_continuity
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
