let S, T be TopSpace; for h being Function of S,T
for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds
g is isomorphic
let h be Function of S,T; for g being Function of (Omega S),(Omega T) st h = g & h is being_homeomorphism holds
g is isomorphic
let g be Function of (Omega S),(Omega T); ( h = g & h is being_homeomorphism implies g is isomorphic )
assume that
A1:
h = g
and
A2:
h is being_homeomorphism
; g is isomorphic
A3:
dom h = [#] S
by A2;
A4:
rng h = [#] T
by A2;
A5:
the carrier of T = the carrier of (Omega T)
by Lm1;
A6:
the carrier of S = the carrier of (Omega S)
by Lm1;
A7:
h is one-to-one
by A2;
per cases
( ( not S is empty & not T is empty ) or S is empty or T is empty )
;
suppose A8:
( not
S is
empty & not
T is
empty )
;
g is isomorphic then reconsider s =
S,
t =
T as non
empty TopSpace ;
reconsider f =
g as
Function of
(Omega s),
(Omega t) ;
for
x,
y being
Element of
(Omega s) holds
(
x <= y iff
f . x <= f . y )
proof
let x,
y be
Element of
(Omega s);
( x <= y iff f . x <= f . y )
A9:
dom f =
[#] S
by A1, A2
.=
the
carrier of
S
;
reconsider Z =
{((f ") . (f . y))} as
Subset of
s by Lm1;
A10:
h " is
being_homeomorphism
by A2, A8, TOPS_2:56;
A11:
f is
onto
by A1, A4, A5, FUNCT_2:def 3;
then A12:
f " = f "
by A1, A7, TOPS_2:def 4;
A13:
dom h = the
carrier of
(Omega s)
by A3, Lm1;
then A14:
y =
(h ") . (h . y)
by A7, FUNCT_1:34
.=
(f ") . (f . y)
by A11, A1, A7, TOPS_2:def 4
;
hereby ( f . x <= f . y implies x <= y )
end;
assume
f . x <= f . y
;
x <= y
then consider Y being
Subset of
t such that A18:
Y = {(f . y)}
and A19:
f . x in Cl Y
by Def2;
A20:
f " = h "
by A1, A5, A6;
A21:
x = (f ") . (f . x)
by A1, A7, A12, A13, FUNCT_1:34;
(f ") . (f . x) in (f ") .: (Cl Y)
by A19, FUNCT_2:35;
then A22:
(h ") . (h . x) in Cl ((h ") .: Y)
by A1, A10, A20, TOPS_2:60;
(f ") .: Y =
f " Y
by A1, A7, A12, FUNCT_1:85
.=
Z
by A1, A6, A7, A18, A14, A9, FINSEQ_5:4
;
hence
x <= y
by A1, A20, A22, A21, A14, Def2;
verum
end; hence
g is
isomorphic
by A1, A5, A7, A4, WAYBEL_0:66;
verum end;