|
%------------------------------------------------------------------------------
% Homeomorphism definition file
%
% All references are to WA Sutherland "Introduction to Metric and
% Topological Spaces", OUP, 1981
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 8/7/04 Initial Version
% Version 1.1 8/6/06 Interface Change
%------------------------------------------------------------------------------
homeomorphism_def[T1:Type, (IMPORTING topology_def[T1]) S:topology[T1],
T2:Type, (IMPORTING topology_def[T2]) T:topology[T2]]: THEORY
BEGIN
IMPORTING continuity_def,
continuity[T1,S,T2,T],
continuity[T2,T,T1,S],
structures@function_image_bis[T1,T2] % Proof only
A: VAR topology[T1]
B: VAR topology[T2]
X: VAR set[T1]
f: VAR [T1->T2]
homeomorphism?(f): bool = bijective?[T1,T2](f) AND
continuous?[T1,S,T2,T](f) AND
continuous?[T2,T,T1,S](inverse_alt(f))
homeomorphism: TYPE = (homeomorphism?)
homeomorphism_def: LEMMA
homeomorphism?(f) IFF
(bijective?[T1,T2](f) AND
(FORALL X: open?[T1,S](X) IFF open?[T2,T](image(f,X))))
homeomorphic?(A,B): bool = EXISTS f: homeomorphism?(f)
END homeomorphism_def
¤ Dauer der Verarbeitung: 0.31 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.
|
