|
%------------------------------------------------------------------------------
% composition of metric continuous functions
%
% Author: David Lester, Manchester University
%
% Version 1.0 17/08/07 Initial Version
%------------------------------------------------------------------------------
composition_continuous[T1:TYPE, (IMPORTING metric_def[T1]) d1:metric[T1],
T2:TYPE, (IMPORTING metric_def[T2]) d2:metric[T2],
T3:TYPE, (IMPORTING metric_def[T3]) d3:metric[T3]]
: THEORY
BEGIN
IMPORTING metric_space[T1,d1],
metric_space[T2,d2],
metric_space[T3,d3],
metric_continuity[T1,d1,T2,d2],
metric_continuity[T2,d2,T3,d3],
metric_continuity[T1,d1,T3,d3]
f: VAR [T2->T3]
g: VAR [T1->T2]
composition_continuous: LEMMA metric_continuous?(g) AND
metric_continuous?(f) =>
metric_continuous?(f o g)
END composition_continuous
¤ Dauer der Verarbeitung: 0.19 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.
|
