%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properties of continuous functions [T1 -> T2] % % Applications of continuity_interval % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% inverse_continuous_functions [ T1, T2 : NONEMPTY_TYPE FROM real ] : THEORY BEGIN ASSUMING % BUG: T1_pred is not correctly expanded % connected_domain : ASSUMPTION % FORALL (x, y : T1), (z : real) : % x <= z AND z <= y IMPLIES T1_pred(z) 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 : PROPOSITION bijective?[T1, T2](g) IMPLIES continuous(inverse(g)) END inverse_continuous_functions