%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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