%------------------------------------------------------------------------------ % 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))
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.
