|
lim_of_composition [ T1, T2 : TYPE FROM real ] : THEORY
%----------------------------------------------------------------------------
% Author: Bruno Dutertre Royal Holloway & Bedford New College
%----------------------------------------------------------------------------
BEGIN
IMPORTING lim_of_functions, continuous_functions[T2]
f : VAR [T1 -> T2]
g : VAR [T2 -> real]
x, y : VAR real
z : VAR T2
l : VAR real
adherence_lemma : LEMMA convergence(f, x, y)
IMPLIES adh[T2](fullset[real])(y)
adherence_lemma2 : LEMMA convergent?(f, x)
IMPLIES adh[T2](fullset[real])(lim(f, x))
convergence_composition : LEMMA convergence(f, x, y) AND convergence(g, y, l)
IMPLIES convergence(g o f, x, l)
convergent_composition : LEMMA convergent?(f, x) AND convergent?(g, lim(f, x))
IMPLIES convergent?(g o f, x)
lim_composition : LEMMA convergent?(f, x) AND convergent?(g, lim(f, x))
IMPLIES lim(g o f, x) = lim(g, lim(f, x))
convergence_comp_continuous: LEMMA convergence(f, x, z) AND continuous?(g, z)
IMPLIES convergence(g o f, x, g(z))
convergent_comp_continuous : LEMMA convergent?(f, x) AND T2_pred(lim(f, x))
AND continuous?(g, lim(f, x))
IMPLIES convergent?(g o f, x)
lim_comp_continuous : LEMMA convergent?(f, x) AND T2_pred(lim(f, x))
AND continuous?(g, lim(f, x))
IMPLIES
lim(g o f, x) = g(lim(f, x))
END lim_of_composition
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
