|
real_fun_on_compact_sets[T:TYPE+,d:[T,T->nnreal]]: THEORY
%------------------------------------------------------------------------------
% In This Theory, We Prove That A Continuous Real-Valued Function On A
% Compact Subset Of A Metric Space Attains A Maximum
%
% Authors: Anthony Narkawicz, NASA Langley
%
% Version 1.0 8/31/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: VAR [T -> real]
cont_on_compact_max: THEOREM
(continuous?(f,S) and compact?(S))
IMPLIES empty?(S) or (EXISTS (s: (S)): FORALL (t: (S)): f(t) <= f(s))
cont_on_compact_min: THEOREM
(continuous?(f,S) and compact?(S))
IMPLIES empty?(S) or (EXISTS (s: (S)): FORALL (t: (S)): f(t) >= f(s))
END real_fun_on_compact_sets
¤ Dauer der Verarbeitung: 0.0 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.
|
