let S, T be non empty TopSpace; 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; 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; 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; 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); ( 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
; FUNCT_2:def 3 g is open
let A be Subset of (S | S1); T_0TOPSP:def 2 ( not A is open or g .: A is open )
A5:
[#] (T | T1) = T1
by PRE_TOPC:def 5;
assume
A is open
; g .: A is open
then consider C being Subset of S such that
A6:
C is open
and
A7:
C /\ ([#] (S | S1)) = A
by TOPS_2:24;
A8:
( [#] (S | S1) = S1 & g .: (C /\ S1) c= (g .: C) /\ (g .: S1) )
by PRE_TOPC:def 5, RELAT_1:121;
A9:
g .: A = (f .: C) /\ T1
proof
g .: C c= f .: C
by A1, RELAT_1:128;
then
(g .: C) /\ (g .: S1) c= (f .: C) /\ T1
by A5, XBOOLE_1:27;
hence
g .: A c= (f .: C) /\ T1
by A7, A8;
XBOOLE_0:def 10 (f .: C) /\ T1 c= g .: A
let y be
object ;
TARSKI:def 3 ( not y in (f .: C) /\ T1 or y in g .: A )
A10:
(
dom g c= dom f &
dom f = the
carrier of
S )
by A1, FUNCT_2:def 1, RELAT_1:60;
assume A11:
y in (f .: C) /\ T1
;
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:65;
y in T1
by A11, XBOOLE_0:def 4;
then consider a being
object such that A14:
a in dom g
and A15:
g . a = y
by A2, A5, FUNCT_1:def 3;
f . a = g . a
by A1, A14, FUNCT_1:47;
then
a = x
by A4, A13, A14, A15, A10, FUNCT_1:def 4;
then
a in A
by A7, A12, A14, XBOOLE_0:def 4;
hence
y in g .: A
by A14, A15, FUNCT_1:def 6;
verum
end;
f .: C is open
by A3, A6;
hence
g .: A is open
by A5, A9, TOPS_2:24; verum