let S, T be non empty TopSpace; :: thesis: for S1 being Subset of S
for T1 being Subset of T
for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let S1 be Subset of S; :: thesis: for T1 being Subset of T
for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let T1 be Subset of T; :: thesis: for f being Function of S,T
for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let f be Function of S,T; :: thesis: for g being Function of (S | S1),(T | T1) st g = f | S1 & g is onto & f is open & f is one-to-one holds
g is open
let g be Function of (S | S1),(T | T1); :: thesis: ( g = f | S1 & g is onto & f is open & f is one-to-one implies g is open )
assume that
A1:
g = f | S1
and
A2:
rng g = the carrier of (T | T1)
and
A3:
f is open
and
A4:
f is one-to-one
; :: according to FUNCT_2:def 3 :: thesis: g is open
let A be Subset of (S | S1); :: according to T_0TOPSP:def 2 :: thesis: ( not A is open or g .: A is open )
assume
A is open
; :: thesis: g .: A is open
then consider C being Subset of S such that
A5:
C is open
and
A6:
C /\ ([#] (S | S1)) = A
by TOPS_2:32;
A7:
f .: C is open
by A3, A5, T_0TOPSP:def 2;
A8:
[#] (T | T1) = T1
by PRE_TOPC:def 10;
A9:
[#] (S | S1) = S1
by PRE_TOPC:def 10;
A10:
g .: (C /\ S1) c= (g .: C) /\ (g .: S1)
by RELAT_1:154;
g .: A = (f .: C) /\ T1
proof
g .: C c= f .: C
by A1, RELAT_1:161;
then
(g .: C) /\ (g .: S1) c= (f .: C) /\ T1
by A8, XBOOLE_1:27;
hence
g .: A c= (f .: C) /\ T1
by A6, A9, A10, XBOOLE_1:1;
:: according to XBOOLE_0:def 10 :: thesis: (f .: C) /\ T1 c= g .: A
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in (f .: C) /\ T1 or y in g .: A )
assume A11:
y in (f .: C) /\ T1
;
:: thesis: y in g .: A
then
y in f .: C
by XBOOLE_0:def 4;
then consider x being
Element of
S such that A12:
x in C
and A13:
y = f . x
by FUNCT_2:116;
y in T1
by A11, XBOOLE_0:def 4;
then consider a being
set such that A14:
a in dom g
and A15:
g . a = y
by A2, A8, FUNCT_1:def 5;
A16:
dom g c= dom f
by A1, RELAT_1:89;
A17:
dom f = the
carrier of
S
by FUNCT_2:def 1;
f . a = g . a
by A1, A14, FUNCT_1:70;
then
a = x
by A4, A13, A14, A15, A16, A17, FUNCT_1:def 8;
then
a in A
by A6, A12, A14, XBOOLE_0:def 4;
hence
y in g .: A
by A14, A15, FUNCT_1:def 12;
:: thesis: verum
end;
hence
g .: A is open
by A7, A8, TOPS_2:32; :: thesis: verum