| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 kB |
|
Quelle continuous_functions_props.pvs Sprache: PVS |
|||||||||
|
continuous_functions_props[ T : TYPE FROM real] : THEORY
%-------------------------------------------------------- % More properties of continuous functions [T1 -> T2] % % Applications of continuity_interval % %-------------------------------------------------------- BEGIN ASSUMING connected_domain : ASSUMPTION FORALL (x, y : T), (z : real) : x <= z AND z <= y IMPLIES T_pred(z) ENDASSUMING IMPORTING continuity_interval f : VAR [T -> real] a, b, c, d : VAR T sub_interval : LEMMA FORALL (c : T), (d : {x : T | c <= x}), (u : J[c, d]) : T_pred(u) %---------------------------------------- % Restriction to a sub-interval of T1 %---------------------------------------- R(f, (c : T), (d : {x : T | c <= x})) : [J[c,d] -> real] = LAMBDA (u : J[c, d]) : f(u) %----------------------------------------------------- % If f is continuous, its restriction is continuous %----------------------------------------------------- g : VAR { f | continuous?(f) } continuous_in_subintervals : LEMMA a <= b IMPLIES continuous?(R(g, a, b)) %------------------------------ % Intermediate value theorem %------------------------------ x, y, z : VAR real intermediate1 : LEMMA a <= b AND g(a) <= x AND x <= g(b) IMPLIES EXISTS c : a <= c AND c <= b AND g(c) = x intermediate2 : LEMMA a <= b AND g(b) <= x AND x <= g(a) IMPLIES EXISTS c : a <= c AND c <= b AND g(c) = x %---------------------------------- % Max and minimum in an interval %---------------------------------- max_in_interval : LEMMA a <= b IMPLIES EXISTS c : a <= c AND c <= b AND (FORALL d : a <= d AND d <= b IMPLIES g(d) <= g(c)) min_in_interval : LEMMA a <= b IMPLIES EXISTS c : a <= c AND c <= b AND (FORALL d : a <= d AND d <= b IMPLIES g(c) <= g(d)) %--------------------------------------------------------- % Injective, continuous functions are strictly monotone %--------------------------------------------------------- inj_continuous : LEMMA injective?(g) AND a <= b AND b <= c IMPLIES (g(a) <= g(b) AND g(b) <= g(c)) OR (g(c) <= g(b) AND g(b) <= g(a)) inj_monotone : LEMMA injective?(g) IFF strict_increasing?(g) OR strict_decreasing?(g) END continuous_functions_props ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28