|
continuity_of_max_min[T:TYPE+,d:[T,T->nnreal]]: THEORY
%------------------------------------------------------------------------------
% In This Theory, We Prove That For Continuous Real-Valued Functions
% f And g On A Metric Space, The Functions max(f,g) And min(f,g)
% Are Also Continuous
%
% Authors: Anthony Narkawicz, NASA Langley
%
% Version 1.0 9/16/2009 Initial Version
%------------------------------------------------------------------------------
BEGIN
ASSUMING IMPORTING metric_spaces_def[T,d]
fullset_metric_space: ASSUMPTION metric_space?[T,d](fullset[T])
ENDASSUMING
S: VAR set[T]
% A continuous function on a compact set realizes a maximum and a minimum
IMPORTING real_metric_space, continuity_ms_def[T,d,real,real_dist], reals@abs_lems,
compactness[T,d]
f,g: VAR [T -> real]
x: VAR T
max_fun(f,g)(x): real = max(f(x),g(x))
min_fun(f,g)(x): real = min(f(x),g(x))
max_min_fun_convert: LEMMA max_fun(-f,-g) = -min_fun(f,g) AND min_fun(-f,-g) = -max_fun(f,g)
AND min_fun(f,g) = -max_fun(-f,-g) AND max_fun(f,g) = -min_fun(-f,-g)
max_fun_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES
continuous?(max_fun(f,g),S)
min_fun_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES
continuous?(min_fun(f,g),S)
END continuity_of_max_min
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
