| 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 inverse_continuous_functions.pvs Sprache: PVS |
|||||||||
|
inverse_continuous_functions [ T1, T2 : NONEMPTY_TYPE FROM real ] : THEORY
%---------------------------------------------------------------------------- % More properties of continuous functions [T1 -> T2] % Applications of continuity_interval %---------------------------------------------------------------------------- BEGIN ASSUMING connected_domain : ASSUMPTION FORALL (x, y : T1), (z : real) : x <= z AND z <= y IMPLIES T1_pred(z) % old bug workaround: T1_pred is not correctly expanded % connected_domain : ASSUMPTION % FORALL (x, y : T1), (z : real) : % x <= z AND z <= y IMPLIES (EXISTS (u : T1) : z = u) ENDASSUMING IMPORTING continuous_functions_props g : VAR { f : [T1 -> T2] | continuous?(f) } %------------------------------------------------------------- % inverse of a continuous, bijective function is continuous %------------------------------------------------------------- inverse_incr : LEMMA bijective?[T1, T2](g) AND strict_increasing?(g) IMPLIES continuous?(inverse(g)) inverse_decr : LEMMA bijective?[T1, T2](g) AND strict_decreasing?(g) IMPLIES continuous?(inverse(g)) inverse_continuous : LEMMA bijective?[T1, T2](g) IMPLIES continuous?(inverse(g)) END inverse_continuous_functions ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28