%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Composition of continuous functions %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
composition_continuous [ T1, T2 : TYPE FROM real ] : THEORY
BEGIN
IMPORTING continuous_functions, real_fun_props
f : VAR [T1 -> T2]
g : VAR [T2 -> real]
x0 : VAR T1
F : VAR { E : setof[real] | subset?(E, T1_pred) }
composition_continuous1 : PROPOSITION
continuous(f, x0) AND continuous(g, f(x0))
IMPLIES continuous(g o f, x0)
composition_continuous2 : PROPOSITION
continuous(f, F) AND continuous(g, Im(f, F))
IMPLIES continuous(g o f, F)
composition_continuous3 : PROPOSITION
continuous(f) AND continuous(g) IMPLIES continuous(g o f)
END composition_continuous