let X be non empty TopSpace; ex f being Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) st
( f is isomorphic & ( for V being open Subset of X holds f . V = chi (V, the carrier of X) ) )
deffunc H1( set ) -> Element of bool [: the carrier of X,{0,1}:] = chi ($1, the carrier of X);
consider f being Function such that
A1:
dom f = the topology of X
and
A2:
for a being set st a in the topology of X holds
f . a = H1(a)
from FUNCT_1:sch 5();
A3:
rng f c= the carrier of (oContMaps (X,Sierpinski_Space))
proof
let x be
object ;
TARSKI:def 3 ( not x in rng f or x in the carrier of (oContMaps (X,Sierpinski_Space)) )
assume
x in rng f
;
x in the carrier of (oContMaps (X,Sierpinski_Space))
then consider a being
object such that A4:
a in dom f
and A5:
x = f . a
by FUNCT_1:def 3;
reconsider a =
a as
Subset of
X by A1, A4;
a is
open
by A1, A4, PRE_TOPC:def 2;
then
chi (
a, the
carrier of
X) is
continuous Function of
X,
Sierpinski_Space
by YELLOW16:46;
then
x is
continuous Function of
X,
Sierpinski_Space
by A1, A2, A4, A5;
then
x is
Element of
(oContMaps (X,Sierpinski_Space))
by Th2;
hence
x in the
carrier of
(oContMaps (X,Sierpinski_Space))
;
verum
end;
set S = InclPoset the topology of X;
A6:
the carrier of (InclPoset the topology of X) = the topology of X
by YELLOW_1:1;
then reconsider f = f as Function of (InclPoset the topology of X),(oContMaps (X,Sierpinski_Space)) by A1, A3, FUNCT_2:2;
A7:
now for x, y being Element of (InclPoset the topology of X) holds
( x <= y iff f . x <= f . y )let x,
y be
Element of
(InclPoset the topology of X);
( x <= y iff f . x <= f . y )
(
x in the
topology of
X &
y in the
topology of
X )
by A6;
then reconsider V =
x,
W =
y as
open Subset of
X by PRE_TOPC:def 2;
set cx =
chi (
V, the
carrier of
X);
set cy =
chi (
W, the
carrier of
X);
A8:
(
f . x = chi (
V, the
carrier of
X) &
f . y = chi (
W, the
carrier of
X) )
by A2, A6;
chi (
V, the
carrier of
X) is
continuous Function of
X,
Sierpinski_Space
by YELLOW16:46;
then A9:
chi (
V, the
carrier of
X) is
Element of
(oContMaps (X,Sierpinski_Space))
by Th2;
chi (
W, the
carrier of
X) is
continuous Function of
X,
Sierpinski_Space
by YELLOW16:46;
then
chi (
W, the
carrier of
X) is
Element of
(oContMaps (X,Sierpinski_Space))
by Th2;
then reconsider cx =
chi (
V, the
carrier of
X),
cy =
chi (
W, the
carrier of
X) as
continuous Function of
X,
(Omega Sierpinski_Space) by A9, Th1;
(
x <= y iff
V c= W )
by YELLOW_1:3;
then
(
x <= y iff
cx <= cy )
by Th4, YELLOW16:49;
hence
(
x <= y iff
f . x <= f . y )
by A8, Th3;
verum end;
set T = oContMaps (X,Sierpinski_Space);
A10:
rng f = the carrier of (oContMaps (X,Sierpinski_Space))
proof
the
topology of
Sierpinski_Space = {{},{1},{0,1}}
by WAYBEL18:def 9;
then
{1} in the
topology of
Sierpinski_Space
by ENUMSET1:def 1;
then reconsider V =
{1} as
open Subset of
Sierpinski_Space by PRE_TOPC:def 2;
thus
rng f c= the
carrier of
(oContMaps (X,Sierpinski_Space))
;
XBOOLE_0:def 10 the carrier of (oContMaps (X,Sierpinski_Space)) c= rng f
let t be
object ;
TARSKI:def 3 ( not t in the carrier of (oContMaps (X,Sierpinski_Space)) or t in rng f )
assume
t in the
carrier of
(oContMaps (X,Sierpinski_Space))
;
t in rng f
then reconsider g =
t as
continuous Function of
X,
Sierpinski_Space by Th2;
[#] Sierpinski_Space <> {}
;
then A11:
g " V is
open
by TOPS_2:43;
then reconsider c =
chi (
(g " V), the
carrier of
X) as
Function of
X,
Sierpinski_Space by YELLOW16:46;
then A13:
g = c
by FUNCT_2:63;
A14:
g " V in the
topology of
X
by A11, PRE_TOPC:def 2;
then
f . (g " V) = chi (
(g " V), the
carrier of
X)
by A2;
hence
t in rng f
by A1, A14, A13, FUNCT_1:def 3;
verum
end;
take
f
; ( f is isomorphic & ( for V being open Subset of X holds f . V = chi (V, the carrier of X) ) )
f is one-to-one
hence
f is isomorphic
by A10, A7, WAYBEL_0:66; for V being open Subset of X holds f . V = chi (V, the carrier of X)
let V be open Subset of X; f . V = chi (V, the carrier of X)
V in the topology of X
by PRE_TOPC:def 2;
hence
f . V = chi (V, the carrier of X)
by A2; verum