let T1, T2 be TopSpace; for A2 being Subset of T2
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
let A2 be Subset of T2; for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
let f be Function of T1,T2; ( f is being_homeomorphism implies for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism )
assume A1:
f is being_homeomorphism
; for g being Function of (T1 | (f " A2)),(T2 | A2) st g = A2 |` f holds
g is being_homeomorphism
A2:
( dom f = [#] T1 & rng f = [#] T2 )
by A1, TOPS_2:def 5;
T1,T2 are_homeomorphic
by A1, T_0TOPSP:def 1;
then
( T1 is empty iff T2 is empty )
by YELLOW14:18;
then A3:
( [#] T1 = {} iff [#] T2 = {} )
;
A4:
rng f = [#] T2
by A1, TOPS_2:def 5;
set A = f " A2;
let g be Function of (T1 | (f " A2)),(T2 | A2); ( g = A2 |` f implies g is being_homeomorphism )
assume A5:
g = A2 |` f
; g is being_homeomorphism
A6:
rng g = A2
by A2, A5, RELAT_1:89;
A7:
f is one-to-one
by A1, TOPS_2:def 5;
then A8:
g is one-to-one
by A5, FUNCT_1:58;
set TA = T1 | (f " A2);
set TB = T2 | A2;
A10:
[#] (T1 | (f " A2)) = f " A2
by PRE_TOPC:def 5;
A11:
( [#] (T1 | (f " A2)) = {} iff [#] (T2 | A2) = {} )
by A6;
A12:
[#] (T2 | A2) = A2
by PRE_TOPC:def 5;
A13:
f is continuous
by A1, TOPS_2:def 5;
for P being Subset of (T2 | A2) st P is open holds
g " P is open
proof
let P be
Subset of
(T2 | A2);
( P is open implies g " P is open )
assume
P is
open
;
g " P is open
then consider P1 being
Subset of
T2 such that A14:
P1 is
open
and A15:
P = P1 /\ A2
by A12, TSP_1:def 1;
A16:
f " P1 is
open
by A3, A13, A14, TOPS_2:43;
g " P =
f " P
by A5, Th2, A15, XBOOLE_1:17
.=
(f " P1) /\ the
carrier of
(T1 | (f " A2))
by A10, A15, FUNCT_1:68
;
hence
g " P is
open
by A16, TSP_1:def 1;
verum
end;
then A17:
g is continuous
by A11, TOPS_2:43;
A18:
f " is continuous
by A1, TOPS_2:def 5;
for P being Subset of (T1 | (f " A2)) st P is open holds
(g ") " P is open
proof
let P be
Subset of
(T1 | (f " A2));
( P is open implies (g ") " P is open )
assume
P is
open
;
(g ") " P is open
then consider P1 being
Subset of
T1 such that A19:
P1 is
open
and A20:
P = P1 /\ (f " A2)
by A10, TSP_1:def 1;
A21:
(f ") " P1 is
open
by A3, A18, A19, TOPS_2:43;
A2 = f .: (f " A2)
by A2, FUNCT_1:77;
then A22:
the
carrier of
(T2 | A2) = (f ") " (f " A2)
by A12, A4, A7, TOPS_2:54;
(g ") " P =
(A2 |` f) .: P
by A5, A6, A8, A12, TOPS_2:54
.=
(f .: P) /\ the
carrier of
(T2 | A2)
by A12, FUNCT_1:67
.=
((f ") " (P1 /\ (f " A2))) /\ the
carrier of
(T2 | A2)
by A4, A7, A20, TOPS_2:54
.=
(((f ") " P1) /\ ((f ") " (f " A2))) /\ the
carrier of
(T2 | A2)
by FUNCT_1:68
.=
((f ") " P1) /\ (((f ") " (f " A2)) /\ the carrier of (T2 | A2))
by XBOOLE_1:16
.=
((f ") " P1) /\ the
carrier of
(T2 | A2)
by A22
;
hence
(g ") " P is
open
by A21, TSP_1:def 1;
verum
end;
then
g " is continuous
by A11, TOPS_2:43;
hence
g is being_homeomorphism
by A6, A5, Th1, A10, A8, A12, A17, TOPS_2:def 5; verum