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 Th14;
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
A1:
dom f = the carrier of T
and
A2:
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 ))
then reconsider f = f as Function of T,(product (M --> Sierpinski_Space )) by A1, FUNCT_2:def 1, RELSET_1:11;
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:12;
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 4;
A13:
i c= f " A
proof
let z be
set ;
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, PRE_TOPC:def 5;
then A15:
i in { u where u is Subset of T : ( z in u & u is open ) }
by A14;
A16:
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 ;
( 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:32;
then A17:
w in M
by PARTFUN1:def 4;
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 5;
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 13;
then A21:
(Carrier (M --> Sierpinski_Space )) . w =
the
carrier of
Sierpinski_Space
by A17, FUNCOP_1:13
.=
{0 ,1}
by Def9
;
((Carrier (M --> Sierpinski_Space )) +* i,V) . w = (Carrier (M --> Sierpinski_Space )) . w
by A19, FUNCT_7:34;
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;
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 4
.=
dom ((Carrier (M --> Sierpinski_Space )) +* i,V)
by FUNCT_7:32
;
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 13;
verum
end;
A24:
((Carrier (M --> Sierpinski_Space )) +* i,V) . i = {1}
by A12, FUNCT_7:33;
f " A c= i
proof
let z be
set ;
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 13;
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
set 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:32;
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:42;
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, XBOOLE_0:def 10;
hence
f " A is
open
by A11, PRE_TOPC:def 5;
verum
end;
then
f is continuous
by YELLOW_9:36;
then A27:
( dom (corestr f) = [#] T & corestr f is continuous )
by Th11, 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
set ;
( 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
set such that A40:
x in dom f
and A41:
x in V
and A42:
y = f . x
by FUNCT_1:def 12;
y in rng f
by A40, A42, FUNCT_1:def 5;
then A43:
y in the
carrier of
(Image f)
by Th10;
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
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 ;
( 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:32;
then A47:
W in M
by PARTFUN1:def 4;
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 5;
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 13;
then A52:
(Carrier (M --> Sierpinski_Space )) . W =
the
carrier of
Sierpinski_Space
by A47, FUNCOP_1:13
.=
{0 ,1}
by Def9
;
((Carrier (M --> Sierpinski_Space )) +* V,{1}) . W = (Carrier (M --> Sierpinski_Space )) . W
by A50, FUNCT_7:34;
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; 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 4
.=
dom ((Carrier (M --> Sierpinski_Space )) +* V,{1})
by FUNCT_7:32
;
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
set ;
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
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;
rng f = the
carrier of
(Image f)
by Th10;
then
y in rng f
by A54, XBOOLE_0:def 4;
then consider x being
set such that A57:
(
x in dom f &
y = f . x )
by FUNCT_1:def 5;
V in the
topology of
T
by A39, PRE_TOPC:def 5;
then
V in M
by YELLOW_1:1;
then A58:
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 A56;
then A59:
g . V in {1}
by A58, FUNCT_7:33;
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:42;
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 12;
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:55;
hence
corestr f is being_homeomorphism
by A8, A28, A27, TOPS_2:def 5; verum