|
composition_continuous [ T1, T2 : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
% Composition of continuous functions
%
% Author: Bruno Dutertre Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN
IMPORTING continuous_functions, reals@real_fun_props
f : VAR [T1 -> T2]
g : VAR [T2 -> real]
x0 : VAR T1
F : VAR { E : setof[real] | subset?(E, T1_pred) }
composition_cont : LEMMA continuous?(f, x0) AND continuous?(g, f(x0))
IMPLIES continuous?(g o f, x0)
composition_cont_set : LEMMA continuous_on?(f, F) AND continuous_on?(g, Im(f, F))
IMPLIES continuous_on?(g o f, F)
composition_cont_fun : LEMMA continuous?(f) AND continuous?(g)
IMPLIES continuous?(g o f)
END composition_continuous
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
