let X be non empty TopSpace; :: thesis: 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,{{} ,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 3();
A3:
the carrier of (InclPoset the topology of X) = the topology of X
by YELLOW_1:1;
rng f c= the carrier of (oContMaps X,Sierpinski_Space )
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in the carrier of (oContMaps X,Sierpinski_Space ) )
assume
x in rng f
;
:: thesis: x in the carrier of (oContMaps X,Sierpinski_Space )
then consider a being
set such that A4:
(
a in dom f &
x = f . a )
by FUNCT_1:def 5;
reconsider a =
a as
Subset of
X by A1, A4;
a is
open
by A1, A4, PRE_TOPC:def 5;
then
chi a,the
carrier of
X is
continuous Function of
X,
Sierpinski_Space
by YELLOW16:48;
then
x is
continuous Function of
X,
Sierpinski_Space
by A1, A2, A4;
then
x is
Element of
(oContMaps X,Sierpinski_Space )
by Th2;
hence
x in the
carrier of
(oContMaps X,Sierpinski_Space )
;
:: thesis: verum
end;
then reconsider f = f as Function of (InclPoset the topology of X),(oContMaps X,Sierpinski_Space ) by A1, A3, FUNCT_2:4;
take
f
; :: thesis: ( f is isomorphic & ( for V being open Subset of X holds f . V = chi V,the carrier of X ) )
set S = InclPoset the topology of X;
set T = oContMaps X,Sierpinski_Space ;
A5:
f is one-to-one
A6:
rng f = the carrier of (oContMaps X,Sierpinski_Space )
proof
thus
rng f c= the
carrier of
(oContMaps X,Sierpinski_Space )
;
:: according to XBOOLE_0:def 10 :: thesis: the carrier of (oContMaps X,Sierpinski_Space ) c= rng f
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 )
;
:: thesis: t in rng f
then reconsider g =
t as
continuous Function of
X,
Sierpinski_Space by Th2;
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 5;
[#] Sierpinski_Space <> {}
;
then A7:
g " V is
open
by TOPS_2:55;
then A8:
g " V in the
topology of
X
by PRE_TOPC:def 5;
then A9:
f . (g " V) = chi (g " V),the
carrier of
X
by A2;
reconsider c =
chi (g " V),the
carrier of
X as
Function of
X,
Sierpinski_Space by A7, YELLOW16:48;
then
g = c
by FUNCT_2:113;
hence
t in rng f
by A1, A8, A9, FUNCT_1:def 5;
:: thesis: verum
end;
now let x,
y be
Element of
(InclPoset the topology of X);
:: thesis: ( x <= y iff f . x <= f . y )
(
x in the
topology of
X &
y in the
topology of
X )
by A3;
then reconsider V =
x,
W =
y as
open Subset of
X by PRE_TOPC:def 5;
set cx =
chi V,the
carrier of
X;
set cy =
chi W,the
carrier of
X;
A11:
(
f . x = chi V,the
carrier of
X &
f . y = chi W,the
carrier of
X )
by A2, A3;
(
chi V,the
carrier of
X is
continuous Function of
X,
Sierpinski_Space &
chi W,the
carrier of
X is
continuous Function of
X,
Sierpinski_Space )
by YELLOW16:48;
then
(
chi V,the
carrier of
X is
Element of
(oContMaps X,Sierpinski_Space ) &
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 Th1;
(
x <= y iff
V c= W )
by YELLOW_1:3;
then
(
x <= y iff
cx <= cy )
by Th4, YELLOW16:51;
hence
(
x <= y iff
f . x <= f . y )
by A11, Th3;
:: thesis: verum end;
hence
f is isomorphic
by A5, A6, WAYBEL_0:66; :: thesis: for V being open Subset of X holds f . V = chi V,the carrier of X
let V be open Subset of X; :: thesis: f . V = chi V,the carrier of X
V in the topology of X
by PRE_TOPC:def 5;
hence
f . V = chi V,the carrier of X
by A2; :: thesis: verum