%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properties of continuous functions [T1 -> T2] % % Applications of continuity_interval % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% continuous_functions_props[ T : TYPE FROM real] : THEORY 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 : PROPOSITION a <= b AND g(a) <= x AND x <= g(b) IMPLIES EXISTS c : a <= c AND c <= b AND g(c) = x intermediate2 : PROPOSITION 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 : PROPOSITION 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 : PROPOSITION 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 : PROPOSITION injective?(g) IFF strict_increasing(g) OR strict_decreasing(g) END continuous_functions_props