%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Properties of continuous functions %
% in relation with sequences, limits %
% and points of accumulation %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
continuity_props[T : TYPE FROM real] : THEORY
BEGIN
IMPORTING continuous_functions, top_sequences
f : VAR [T -> real]
u : VAR sequence[T]
l, a : VAR T
%--------------------------------------------
% u is convergent to l and f is continuous
%--------------------------------------------
continuity_limit : PROPOSITION
convergence(u, l) AND continuous(f, l)
IMPLIES convergence(f o u, f(l))
%--------------------------------------------
% point of accumulation
%--------------------------------------------
continuity_accumulation : PROPOSITION
accumulation(u, a) AND continuous(f, a)
IMPLIES accumulation(f o u, f(a))
END continuity_props