%--------------------------------------------------------------------------------------------------------- % % One-Variable Uniform Continuity of Real Valued Functions on Product Metric Spaces % % Author: Anthony Narkawicz, NASA Langley % % % Version 1.0 August 27, 2009 % %---------------------------------------------------------------------------------------------------------
cross_metric_real_fun[T1:Type+,d1:[T1,T1->nnreal],
T2:Type+,d2:[T2,T2->nnreal]]: THEORY
X: VAR set[T1]
Y: VAR set[T2]
f: VAR [[T1,T2] -> real]
% If X is compact, then the function unif_min_first(f,X) = (LAMBDA (t: T2) = min({r: real | EXISTS (x: (X)): r = f(x,t)})) % is continuous.
IMPORTING reals@bounded_reals[real]
% The main TCC:
curried_min_exists: LEMMAnonempty?(X) AND continuous?(f,fullset[[(X),(Y)]]) AND compact?(X) IMPLIES (FORALL (t: T2): Y(t) IMPLIES nonempty?[real]({r: real | EXISTS (x: (X)): r = f(x, t)}) AND
below_bounded[real]({r: real | EXISTS (x: (X)): r = f(x, t)}) AND
ext[real]({r: real | EXISTS (x: (X)): r = f(x, t)})(inf[real]({r: real | EXISTS (x: (X)): r = f(x, t)})) AND (EXISTS (x: (X)): FORALL (y: (X)): f(x,t) <= f(y,t)))
curried_min_is_cont: THEOREM (compact?(X) AND continuous?(f,fullset[[(X),(Y)]]) ANDnonempty?(X)) IMPLIES LET unif_min_first(t: T2): real = IF Y(t) THEN min({r: real | EXISTS (x: (X)): r = f(x,t)}) ELSE 0 ENDIF IN continuous?(unif_min_first,Y)
END cross_metric_real_fun
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
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.
