| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: PVSOriginal von: PVS© |
|
||||||
|
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.39 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
