let T1, T2 be TopSpace; for A1 being Subset of T1
for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism
let A1 be Subset of T1; for f being Function of T1,T2 st f is being_homeomorphism holds
for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism
let f be Function of T1,T2; ( f is being_homeomorphism implies for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism )
assume A1:
f is being_homeomorphism
; for g being Function of (T1 | A1),(T2 | (f .: A1)) st g = f | A1 holds
g is being_homeomorphism
A2:
dom f = [#] T1
by A1;
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;
set B = f .: A1;
let g be Function of (T1 | A1),(T2 | (f .: A1)); ( g = f | A1 implies g is being_homeomorphism )
assume A5:
g = f | A1
; g is being_homeomorphism
A6:
rng g = f .: A1
by A5, RELAT_1:115;
A7:
f is one-to-one
by A1;
then A8:
g is one-to-one
by A5, FUNCT_1:52;
A9: dom g =
(dom f) /\ A1
by A5, RELAT_1:61
.=
A1
by A2, XBOOLE_1:28
;
set TA = T1 | A1;
set TB = T2 | (f .: A1);
A10:
[#] (T1 | A1) = A1
by PRE_TOPC:def 5;
A11:
( [#] (T1 | A1) = {} iff [#] (T2 | (f .: A1)) = {} )
by A9;
A12:
[#] (T2 | (f .: A1)) = f .: A1
by PRE_TOPC:def 5;
A13:
f is continuous
by A1;
for P being Subset of (T2 | (f .: A1)) st P is open holds
g " P is open
proof
let P be
Subset of
(T2 | (f .: A1));
( 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 /\ (f .: A1)
by A12, TSP_1:def 1;
reconsider PA =
(f " P1) /\ A1 as
Subset of
(T1 | A1) by A10, XBOOLE_1:17;
A1 = f " (f .: A1)
by A2, A7, FUNCT_1:94;
then
(
A1 /\ PA = PA &
PA = f " P )
by A15, FUNCT_1:68, XBOOLE_1:17, XBOOLE_1:28;
then A16:
g " P = PA
by A5, FUNCT_1:70;
f " P1 is
open
by A3, A13, A14, TOPS_2:43;
hence
g " P is
open
by A10, A16, TSP_1:def 1;
verum
end;
then A17:
g is continuous
by A11, TOPS_2:43;
A18:
f " is continuous
by A1;
for P being Subset of (T1 | A1) st P is open holds
(g ") " P is open
proof
let P be
Subset of
(T1 | A1);
( 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 /\ A1
by A10, TSP_1:def 1;
reconsider PB =
((f ") " P1) /\ (f .: A1) as
Subset of
(T2 | (f .: A1)) by A12, XBOOLE_1:17;
A21:
(f ") " P1 is
open
by A3, A18, A19, TOPS_2:43;
f .: A1 = (f ") " A1
by A4, A7, TOPS_2:54;
then PB =
(f ") " (P1 /\ A1)
by FUNCT_1:68
.=
f .: P
by A4, A7, A20, TOPS_2:54
.=
g .: P
by A5, A10, RELAT_1:129
.=
(g ") " P
by A6, A8, A12, TOPS_2:54
;
hence
(g ") " P is
open
by A12, A21, TSP_1:def 1;
verum
end;
then
g " is continuous
by A11, TOPS_2:43;
hence
g is being_homeomorphism
by A6, A9, A10, A8, A12, A17; verum