| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle real_fun_on_compact_sets.pvs Sprache: 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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28