let T be T_0-TopSpace; :: thesis: ex M being non empty set ex f being Function of T,(product (M --> Sierpinski_Space )) st corestr f is being_homeomorphism
A1:
[#] T <> {}
;
take M = the carrier of (InclPoset the topology of T); :: thesis: ex f being Function of T,(product (M --> Sierpinski_Space )) st corestr f is being_homeomorphism
set J = M --> Sierpinski_Space ;
deffunc H1( set ) -> Element of bool [:the topology of T,{{} ,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
A2:
dom f = the carrier of T
and
A3:
for x being set 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 ))
proof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of (product (M --> Sierpinski_Space )) )
assume
y in rng f
;
:: thesis: y in the carrier of (product (M --> Sierpinski_Space ))
then consider x being
set such that A4:
x in dom f
and A5:
y = f . x
by FUNCT_1:def 5;
set ch =
chi { u where u is Subset of T : ( x in u & u is open ) } ,the
topology of
T;
A6:
y = chi { u where u is Subset of T : ( x in u & u is open ) } ,the
topology of
T
by A2, A3, A4, A5;
A7:
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 4
;
for
z being
set st
z in dom (Carrier (M --> Sierpinski_Space )) holds
(chi { u where u is Subset of T : ( x in u & u is open ) } ,the topology of T) . z in (Carrier (M --> Sierpinski_Space )) . z
proof
let z be
set ;
:: thesis: ( z in dom (Carrier (M --> Sierpinski_Space )) implies (chi { u where u is Subset of T : ( x in u & u is open ) } ,the topology of T) . z in (Carrier (M --> Sierpinski_Space )) . z )
assume
z in dom (Carrier (M --> Sierpinski_Space ))
;
:: thesis: (chi { u where u is Subset of T : ( x in u & u is open ) } ,the topology of T) . z in (Carrier (M --> Sierpinski_Space )) . z
then A8:
z in M
by PARTFUN1:def 4;
then A9:
z in the
topology of
T
by YELLOW_1:1;
consider R being
1-sorted such that A10:
R = (M --> Sierpinski_Space ) . z
and A11:
(Carrier (M --> Sierpinski_Space )) . z = the
carrier of
R
by A8, PRALG_1:def 13;
A12:
(Carrier (M --> Sierpinski_Space )) . z =
the
carrier of
Sierpinski_Space
by A8, A10, A11, FUNCOP_1:13
.=
{0 ,1}
by Def9
;
z in dom (chi { u where u is Subset of T : ( x in u & u is open ) } ,the topology of T)
by A9, FUNCT_3:def 3;
then
(chi { u where u is Subset of T : ( x in u & u is open ) } ,the topology of T) . z in rng (chi { u where u is Subset of T : ( x in u & u is open ) } ,the topology of T)
by FUNCT_1:def 5;
hence
(chi { u where u is Subset of T : ( x in u & u is open ) } ,the topology of T) . z in (Carrier (M --> Sierpinski_Space )) . z
by A12;
:: thesis: verum
end;
then
y in product (Carrier (M --> Sierpinski_Space ))
by A6, A7, CARD_3:def 5;
hence
y in the
carrier of
(product (M --> Sierpinski_Space ))
by Def3;
:: thesis: verum
end;
then reconsider f = f as Function of T,(product (M --> Sierpinski_Space )) by A2, FUNCT_2:def 1, RELSET_1:11;
reconsider PP = { (product ((Carrier (M --> Sierpinski_Space )) +* m,{1})) where m is Element of M : verum } as prebasis of product (M --> Sierpinski_Space ) by Th14;
for A being Subset of (product (M --> Sierpinski_Space )) st A in PP holds
f " A is open
proof
let A be
Subset of
(product (M --> Sierpinski_Space ));
:: thesis: ( A in PP implies f " A is open )
assume A13:
A in PP
;
:: thesis: f " A is open
reconsider a =
A as
Subset of
(product (Carrier (M --> Sierpinski_Space ))) by Def3;
consider i being
Element of
M such that A14:
a = product ((Carrier (M --> Sierpinski_Space )) +* i,{1})
by A13;
A15:
i in M
;
then A16:
i in the
topology of
T
by YELLOW_1:1;
then reconsider i' =
i as
Subset of
T ;
A17:
i in dom (Carrier (M --> Sierpinski_Space ))
by A15, PARTFUN1:def 4;
{1} c= {0 ,1}
by ZFMISC_1:12;
then reconsider V =
{1} as
Subset of
Sierpinski_Space by Def9;
A18:
((Carrier (M --> Sierpinski_Space )) +* i,V) . i = {1}
by A17, FUNCT_7:33;
A19:
f " A c= i
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in f " A or z in i )
assume A20:
z in f " A
;
:: thesis: z in i
then A21:
f . z in a
by FUNCT_1:def 13;
set W =
{ u where u is Subset of T : ( z in u & u is open ) } ;
f . z = chi { u where u is Subset of T : ( z in u & u is open ) } ,the
topology of
T
by A3, A20;
then consider g being
Function such that A22:
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 A23:
for
w being
set st
w in dom ((Carrier (M --> Sierpinski_Space )) +* i,V) holds
g . w in ((Carrier (M --> Sierpinski_Space )) +* i,V) . w
by A14, A21, CARD_3:def 5;
i in dom ((Carrier (M --> Sierpinski_Space )) +* i,V)
by A17, FUNCT_7:32;
then
g . i in ((Carrier (M --> Sierpinski_Space )) +* i,V) . i
by A23;
then
(chi { u where u is Subset of T : ( z in u & u is open ) } ,the topology of T) . i = 1
by A18, A22, TARSKI:def 1;
then
i in { u where u is Subset of T : ( z in u & u is open ) }
by FUNCT_3:42;
then
ex
uu being
Subset of
T st
(
i = uu &
z in uu &
uu is
open )
;
hence
z in i
;
:: thesis: verum
end;
i c= f " A
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in i or z in f " A )
assume A24:
z in i
;
:: thesis: z in f " A
set W =
{ u where u is Subset of T : ( z in u & u is open ) } ;
i' is
open
by A16, PRE_TOPC:def 5;
then A25:
i in { u where u is Subset of T : ( z in u & u is open ) }
by A24;
A26:
z in i'
by A24;
then A27:
f . z = chi { u where u is Subset of T : ( z in u & u is open ) } ,the
topology of
T
by A3;
A28:
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 4
.=
dom ((Carrier (M --> Sierpinski_Space )) +* i,V)
by FUNCT_7:32
;
for
w being
set 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
set ;
:: thesis: ( 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)
;
:: thesis: (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:32;
then A29:
w in M
by PARTFUN1:def 4;
then
w in the
topology of
T
by YELLOW_1:1;
then A30:
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
w <> i
;
:: thesis: (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) . wthen A33:
((Carrier (M --> Sierpinski_Space )) +* i,V) . w = (Carrier (M --> Sierpinski_Space )) . w
by FUNCT_7:34;
consider r being
1-sorted such that A34:
r = (M --> Sierpinski_Space ) . w
and A35:
(Carrier (M --> Sierpinski_Space )) . w = the
carrier of
r
by A29, PRALG_1:def 13;
A36:
(Carrier (M --> Sierpinski_Space )) . w =
the
carrier of
Sierpinski_Space
by A29, A34, A35, FUNCOP_1:13
.=
{0 ,1}
by Def9
;
(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 A30, FUNCT_1:def 5;
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 A33, A36;
:: thesis: verum end;
end;
then
f . z in A
by A14, A27, A28, CARD_3:def 5;
hence
z in f " A
by A2, A26, FUNCT_1:def 13;
:: thesis: verum
end;
then
f " A = i
by A19, XBOOLE_0:def 10;
hence
f " A is
open
by A16, PRE_TOPC:def 5;
:: thesis: verum
end;
then A37:
f is continuous
by YELLOW_9:36;
take
f
; :: thesis: corestr f is being_homeomorphism
A38:
dom (corestr f) = [#] T
by FUNCT_2:def 1;
A39:
rng (corestr f) = [#] (Image f)
by FUNCT_2:def 3;
A40:
corestr f is one-to-one
A51:
corestr f is continuous
by A37, Th11;
A52:
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;
:: thesis: ( V is open implies f .: V = (product ((Carrier (M --> Sierpinski_Space )) +* V,{1})) /\ the carrier of (Image f) )
assume A53:
V is
open
;
:: thesis: f .: V = (product ((Carrier (M --> Sierpinski_Space )) +* V,{1})) /\ the carrier of (Image f)
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: (product ((Carrier (M --> Sierpinski_Space )) +* V,{1})) /\ the carrier of (Image f) c= f .: V
let y be
set ;
:: thesis: ( y in f .: V implies y in (product ((Carrier (M --> Sierpinski_Space )) +* V,{1})) /\ the carrier of (Image f) )assume
y in f .: V
;
:: thesis: y in (product ((Carrier (M --> Sierpinski_Space )) +* V,{1})) /\ the carrier of (Image f)then consider x being
set such that A54:
x in dom f
and A55:
x in V
and A56:
y = f . x
by FUNCT_1:def 12;
set Q =
{ u where u is Subset of T : ( x in u & u is open ) } ;
A57:
V in { u where u is Subset of T : ( x in u & u is open ) }
by A53, A55;
A58:
y = chi { u where u is Subset of T : ( x in u & u is open ) } ,the
topology of
T
by A3, A54, A56;
A59:
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 4
.=
dom ((Carrier (M --> Sierpinski_Space )) +* V,{1})
by FUNCT_7:32
;
for
W being
set 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
set ;
:: thesis: ( 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})
;
:: thesis: (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 A60:
W in dom (Carrier (M --> Sierpinski_Space ))
by FUNCT_7:32;
then A61:
W in M
by PARTFUN1:def 4;
then A62:
W in the
topology of
T
by YELLOW_1:1;
then A63:
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
W <> V
;
:: thesis: (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}) . Wthen A66:
((Carrier (M --> Sierpinski_Space )) +* V,{1}) . W = (Carrier (M --> Sierpinski_Space )) . W
by FUNCT_7:34;
consider r being
1-sorted such that A67:
r = (M --> Sierpinski_Space ) . W
and A68:
(Carrier (M --> Sierpinski_Space )) . W = the
carrier of
r
by A61, PRALG_1:def 13;
A69:
(Carrier (M --> Sierpinski_Space )) . W =
the
carrier of
Sierpinski_Space
by A61, A67, A68, FUNCOP_1:13
.=
{0 ,1}
by Def9
;
(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 A63, FUNCT_1:def 5;
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 A66, A69;
:: thesis: verum end;
end; then A70:
y in product ((Carrier (M --> Sierpinski_Space )) +* V,{1})
by A58, A59, CARD_3:def 5;
y in rng f
by A54, A56, FUNCT_1:def 5;
then
y in the
carrier of
(Image f)
by Th10;
hence
y in (product ((Carrier (M --> Sierpinski_Space )) +* V,{1})) /\ the
carrier of
(Image f)
by A70, XBOOLE_0:def 4;
:: thesis: verum
end;
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in (product ((Carrier (M --> Sierpinski_Space )) +* V,{1})) /\ the carrier of (Image f) or y in f .: V )
assume A71:
y in (product ((Carrier (M --> Sierpinski_Space )) +* V,{1})) /\ the
carrier of
(Image f)
;
:: thesis: y in f .: V
rng f = the
carrier of
(Image f)
by Th10;
then
y in rng f
by A71, XBOOLE_0:def 4;
then consider x being
set such that A72:
x in dom f
and A73:
y = f . x
by FUNCT_1:def 5;
set Q =
{ u where u is Subset of T : ( x in u & u is open ) } ;
A74:
y = chi { u where u is Subset of T : ( x in u & u is open ) } ,the
topology of
T
by A3, A72, A73;
y in product ((Carrier (M --> Sierpinski_Space )) +* V,{1})
by A71, XBOOLE_0:def 4;
then consider g being
Function such that A75:
y = g
and
dom g = dom ((Carrier (M --> Sierpinski_Space )) +* V,{1})
and A76:
for
W being
set 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;
V in the
topology of
T
by A53, PRE_TOPC:def 5;
then
V in M
by YELLOW_1:1;
then A77:
V in dom (Carrier (M --> Sierpinski_Space ))
by PARTFUN1:def 4;
then
V in dom ((Carrier (M --> Sierpinski_Space )) +* V,{1})
by FUNCT_7:32;
then
g . V in ((Carrier (M --> Sierpinski_Space )) +* V,{1}) . V
by A76;
then
g . V in {1}
by A77, FUNCT_7:33;
then
(chi { u where u is Subset of T : ( x in u & u is open ) } ,the topology of T) . V = 1
by A74, A75, TARSKI:def 1;
then
V in { u where u is Subset of T : ( x in u & u is open ) }
by FUNCT_3:42;
then
ex
u being
Subset of
T st
(
u = V &
x in u &
u is
open )
;
hence
y in f .: V
by A72, A73, FUNCT_1:def 12;
:: thesis: verum
end;
for V being Subset of T st V is open holds
((corestr f) " ) " V is open
then
(corestr f) " is continuous
by A1, TOPS_2:55;
hence
corestr f is being_homeomorphism
by A38, A39, A40, A51, TOPS_2:def 5; :: thesis: verum