|
%------------------------------------------------------------------------------
% Product of Complete Metric Spaces
%
% Author: David Lester, Manchester University
%
% Version 1.0 20/12/07 Initial Version
%------------------------------------------------------------------------------
complete_product[T0,T1:TYPE, (IMPORTING metric_def)
d0:metric[T0],d1:metric[T1]]: THEORY
BEGIN
z0,z1: VAR [T0,T1]
IMPORTING reals@sqrt,
metric_space_def[T0,d0],
metric_space_def[T1,d1],
metric_space_def,
metric_def
d2: MACRO metric[[T0,T1]] =
(LAMBDA (z0,z1): sqrt(sq(d0(z0`1,z1`1))+sq(d1(z0`2,z1`2))))
complete_d2: LEMMA metric_complete?(fullset[T0]) AND
metric_complete?(fullset[T1]) =>
metric_complete?[[T0,T1],d2](fullset[[T0,T1]])
END complete_product
¤ Dauer der Verarbeitung: 0.0 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.
|
