|
%------------------------------------------------------------------------------
% Homeomorphisms are Symmetric
%
% 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
%------------------------------------------------------------------------------
homeomorphic_symmetric[T1:TYPE, (IMPORTING topology_def[T1]) S:topology[T1],
T2:TYPE, (IMPORTING topology_def[T2]) T:topology[T2]
]: THEORY
BEGIN
IMPORTING homeomorphism_def,
structures@function_inverse_alt_aux % For proof only
homeomorphic_symmetric: LEMMA homeomorphic?[T1,S,T2,T](S,T) IFF
homeomorphic?[T2,T,T1,S](T,S)
END homeomorphic_symmetric
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
