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