|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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 : LEMMA
convergence(u, l) AND continuous?(f, l)
IMPLIES convergence(f o u, f(l))
%--------------------------------------------
% point of accumulation
%--------------------------------------------
continuity_accumulation : LEMMA
accumulation(u, a) AND continuous?(f, a)
IMPLIES accumulation(f o u, f(a))
END continuity_props
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
