| 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 metric_space_real_fun.pvs Sprache: PVS |
|||||||||
|
metric_space_real_fun[T:TYPE+,d:[T,T->nnreal]]: THEORY
%------------------------------------------------------------------------------ % This Theory Contains Standard Lemmas About Real-Valued Continuous Functions % On An Arbitrary Metric Space % % 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] IMPORTING real_metric_space, continuity_ms_def[T,d,real,real_dist], reals@abs_lems f,g: VAR [T -> real] c: VAR real scal_continuous: LEMMA continuous?(f,S) IMPLIES continuous?(c* f, S) neg_continuous: LEMMA continuous?(f,S) IMPLIES continuous?( -f,S) sum_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES continuous?(f+g,S) diff_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES continuous?(f-g,S) prod_continuous: LEMMA continuous?(f,S) AND continuous?(g,S) IMPLIES continuous?(f*g,S) abs_comp_cont: LEMMA continuous?(f,S) IMPLIES continuous?(abs(f),S) END metric_space_real_fun ¤ Dauer der Verarbeitung: 0.9 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28