let T be T_0-TopSpace; ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism
take M = the carrier of (InclPoset the topology of T); ex f being Function of T,(product (M --> Sierpinski_Space)) st corestr f is being_homeomorphism
set J = M --> Sierpinski_Space;
reconsider PP = { (product ((Carrier (M --> Sierpinski_Space)) +* (m,{1}))) where m is Element of M : verum } as prebasis of (product (M --> Sierpinski_Space)) by Th13;
deffunc H1( object ) -> Element of K19(K20( the topology of T,{0,1})) = chi ( { u where u is Subset of T : ( $1 in u & u is open ) } , the topology of T);
consider f being Function such that
A1:
dom f = the carrier of T
and
A2:
for x being object st x in the carrier of T holds
f . x = H1(x)
from FUNCT_1:sch 3();
rng f c= the carrier of (product (M --> Sierpinski_Space))
then reconsider f = f as Function of T,(product (M --> Sierpinski_Space)) by A1, FUNCT_2:def 1, RELSET_1:4;
take
f
; corestr f is being_homeomorphism
A8:
rng (corestr f) = [#] (Image f)
by FUNCT_2:def 3;
for A being Subset of (product (M --> Sierpinski_Space)) st A in PP holds
f " A is open
proof
{1} c= {0,1}
by ZFMISC_1:7;
then reconsider V =
{1} as
Subset of
Sierpinski_Space by Def9;
let A be
Subset of
(product (M --> Sierpinski_Space));
( A in PP implies f " A is open )
reconsider a =
A as
Subset of
(product (Carrier (M --> Sierpinski_Space))) by Def3;
assume
A in PP
;
f " A is open
then consider i being
Element of
M such that A9:
a = product ((Carrier (M --> Sierpinski_Space)) +* (i,{1}))
;
A10:
i in M
;
then A11:
i in the
topology of
T
by YELLOW_1:1;
then reconsider i9 =
i as
Subset of
T ;
A12:
i in dom (Carrier (M --> Sierpinski_Space))
by A10, PARTFUN1:def 2;
A13:
i c= f " A
proof
let z be
object ;
TARSKI:def 3 ( not z in i or z in f " A )
assume A14:
z in i
;
z in f " A
set W =
{ u where u is Subset of T : ( z in u & u is open ) } ;
i9 is
open
by A11;
then A15:
i in { u where u is Subset of T : ( z in u & u is open ) }
by A14;
A16:
for
w being
object st
w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) holds
(chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
proof
let w be
object ;
( w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) implies (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w )
assume
w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V))
;
(chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
then
w in dom (Carrier (M --> Sierpinski_Space))
by FUNCT_7:30;
then A17:
w in M
;
then
w in the
topology of
T
by YELLOW_1:1;
then A18:
w in dom (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T))
by FUNCT_3:def 3;
per cases
( w = i or w <> i )
;
suppose A19:
w <> i
;
(chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . wA20:
(chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in rng (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T))
by A18, FUNCT_1:def 3;
ex
r being
1-sorted st
(
r = (M --> Sierpinski_Space) . w &
(Carrier (M --> Sierpinski_Space)) . w = the
carrier of
r )
by A17, PRALG_1:def 15;
then A21:
(Carrier (M --> Sierpinski_Space)) . w =
the
carrier of
Sierpinski_Space
by A17, FUNCOP_1:7
.=
{0,1}
by Def9
;
((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w = (Carrier (M --> Sierpinski_Space)) . w
by A19, FUNCT_7:32;
hence
(chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
by A21, A20;
verum end; end;
end;
A22:
dom (chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) =
the
topology of
T
by FUNCT_3:def 3
.=
M
by YELLOW_1:1
.=
dom (Carrier (M --> Sierpinski_Space))
by PARTFUN1:def 2
.=
dom ((Carrier (M --> Sierpinski_Space)) +* (i,V))
by FUNCT_7:30
;
A23:
z in i9
by A14;
then
f . z = chi (
{ u where u is Subset of T : ( z in u & u is open ) } , the
topology of
T)
by A2;
then
f . z in A
by A9, A22, A16, CARD_3:def 5;
hence
z in f " A
by A1, A23, FUNCT_1:def 7;
verum
end;
A24:
((Carrier (M --> Sierpinski_Space)) +* (i,V)) . i = {1}
by A12, FUNCT_7:31;
f " A c= i
proof
let z be
object ;
TARSKI:def 3 ( not z in f " A or z in i )
set W =
{ u where u is Subset of T : ( z in u & u is open ) } ;
assume
z in f " A
;
z in i
then
(
f . z in a &
f . z = chi (
{ u where u is Subset of T : ( z in u & u is open ) } , the
topology of
T) )
by A2, FUNCT_1:def 7;
then consider g being
Function such that A25:
chi (
{ u where u is Subset of T : ( z in u & u is open ) } , the
topology of
T)
= g
and
dom g = dom ((Carrier (M --> Sierpinski_Space)) +* (i,V))
and A26:
for
w being
object st
w in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V)) holds
g . w in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . w
by A9, CARD_3:def 5;
i in dom ((Carrier (M --> Sierpinski_Space)) +* (i,V))
by A12, FUNCT_7:30;
then
g . i in ((Carrier (M --> Sierpinski_Space)) +* (i,V)) . i
by A26;
then
(chi ( { u where u is Subset of T : ( z in u & u is open ) } , the topology of T)) . i = 1
by A24, A25, TARSKI:def 1;
then
i in { u where u is Subset of T : ( z in u & u is open ) }
by FUNCT_3:36;
then
ex
uu being
Subset of
T st
(
i = uu &
z in uu &
uu is
open )
;
hence
z in i
;
verum
end;
then
f " A = i
by A13;
hence
f " A is
open
by A11;
verum
end;
then
f is continuous
by YELLOW_9:36;
then A27:
( dom (corestr f) = [#] T & corestr f is continuous )
by Th10, FUNCT_2:def 1;
A28:
corestr f is one-to-one
A38:
for V being Subset of T st V is open holds
f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)
proof
let V be
Subset of
T;
( V is open implies f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) )
assume A39:
V is
open
;
f .: V = (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)
hereby TARSKI:def 3,
XBOOLE_0:def 10 (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) c= f .: V
let y be
object ;
( y in f .: V implies y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) )assume
y in f .: V
;
y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f)then consider x being
object such that A40:
x in dom f
and A41:
x in V
and A42:
y = f . x
by FUNCT_1:def 6;
y in rng f
by A40, A42, FUNCT_1:def 3;
then A43:
y in the
carrier of
(Image f)
by Th9;
set Q =
{ u where u is Subset of T : ( x in u & u is open ) } ;
A44:
V in { u where u is Subset of T : ( x in u & u is open ) }
by A39, A41;
A45:
for
W being
object st
W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) holds
(chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
proof
let W be
object ;
( W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) implies (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W )
assume
W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))
;
(chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
then A46:
W in dom (Carrier (M --> Sierpinski_Space))
by FUNCT_7:30;
then A47:
W in M
;
then A48:
W in the
topology of
T
by YELLOW_1:1;
then A49:
W in dom (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T))
by FUNCT_3:def 3;
per cases
( W = V or W <> V )
;
suppose A50:
W <> V
;
(chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . WA51:
(chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in rng (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T))
by A49, FUNCT_1:def 3;
ex
r being
1-sorted st
(
r = (M --> Sierpinski_Space) . W &
(Carrier (M --> Sierpinski_Space)) . W = the
carrier of
r )
by A47, PRALG_1:def 15;
then A52:
(Carrier (M --> Sierpinski_Space)) . W =
the
carrier of
Sierpinski_Space
by A47, FUNCOP_1:7
.=
{0,1}
by Def9
;
((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W = (Carrier (M --> Sierpinski_Space)) . W
by A50, FUNCT_7:32;
hence
(chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
by A52, A51;
verum end; end;
end; A53:
dom (chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) =
the
topology of
T
by FUNCT_3:def 3
.=
M
by YELLOW_1:1
.=
dom (Carrier (M --> Sierpinski_Space))
by PARTFUN1:def 2
.=
dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))
by FUNCT_7:30
;
y = chi (
{ u where u is Subset of T : ( x in u & u is open ) } , the
topology of
T)
by A2, A40, A42;
then
y in product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))
by A53, A45, CARD_3:def 5;
hence
y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the
carrier of
(Image f)
by A43, XBOOLE_0:def 4;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the carrier of (Image f) or y in f .: V )
assume A54:
y in (product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))) /\ the
carrier of
(Image f)
;
y in f .: V
then
y in product ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))
by XBOOLE_0:def 4;
then consider g being
Function such that A55:
y = g
and
dom g = dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))
and A56:
for
W being
object st
W in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) holds
g . W in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . W
by CARD_3:def 5;
rng f = the
carrier of
(Image f)
by Th9;
then
y in rng f
by A54, XBOOLE_0:def 4;
then consider x being
object such that A57:
(
x in dom f &
y = f . x )
by FUNCT_1:def 3;
V in the
topology of
T
by A39;
then
V in M
by YELLOW_1:1;
then A58:
V in dom (Carrier (M --> Sierpinski_Space))
by PARTFUN1:def 2;
then
V in dom ((Carrier (M --> Sierpinski_Space)) +* (V,{1}))
by FUNCT_7:30;
then
g . V in ((Carrier (M --> Sierpinski_Space)) +* (V,{1})) . V
by A56;
then A59:
g . V in {1}
by A58, FUNCT_7:31;
set Q =
{ u where u is Subset of T : ( x in u & u is open ) } ;
y = chi (
{ u where u is Subset of T : ( x in u & u is open ) } , the
topology of
T)
by A2, A57;
then
(chi ( { u where u is Subset of T : ( x in u & u is open ) } , the topology of T)) . V = 1
by A55, A59, TARSKI:def 1;
then
V in { u where u is Subset of T : ( x in u & u is open ) }
by FUNCT_3:36;
then
ex
u being
Subset of
T st
(
u = V &
x in u &
u is
open )
;
hence
y in f .: V
by A57, FUNCT_1:def 6;
verum
end;
A60:
for V being Subset of T st V is open holds
((corestr f) ") " V is open
[#] T <> {}
;
then
(corestr f) " is continuous
by A60, TOPS_2:43;
hence
corestr f is being_homeomorphism
by A8, A28, A27, TOPS_2:def 5; verum