YELLOW_8: Baire Spaces, Sober Spaces

theorem Th2: :: YELLOW_8:2

for X being set
for F being Subset-Family of X st F c= Fin X holds
meet F in Fin X

proof end;

theorem Th3: :: YELLOW_8:3

for X being set
for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent

proof end;

theorem Th4: :: YELLOW_8:4

for X, Y being set st X,Y are_equipotent & X is countable holds
Y is countable

proof end;

theorem :: YELLOW_8:5

for X being 1-sorted
for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )

proof end;

theorem Th6: :: YELLOW_8:6

for X being 1-sorted
for F being Subset-Family of X holds Intersect (COMPLEMENT F) = (union F) `

proof end;

theorem Th7: :: YELLOW_8:7

for X being 1-sorted
for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) `

proof end;

theorem :: YELLOW_8:8

for T being non empty TopSpace
for A, B being Subset of T st B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds
A c= C ) holds
A = Cl B by PRE_TOPC:18, TOPS_1:5;

theorem Th9: :: YELLOW_8:9

for T being TopStruct
for B being Basis of T
for V being Subset of T st V is open holds
V = union { G where G is Subset of T : ( G in B & G c= V ) }

proof end;

theorem Th10: :: YELLOW_8:10

for T being TopStruct
for B being Basis of T
for S being Subset of T st S in B holds
S is open

proof end;

theorem :: YELLOW_8:11

for T being non empty TopSpace
for B being Basis of T
for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }

proof end;

definition

let T be non empty TopStruct ;
let x be Point of T;
let F be Subset-Family of T;

attr F is x -quasi_basis means :Def1: :: YELLOW_8:def 1
( x in Intersect F & ( for S being Subset of T st S is open & x in S holds
ex V being Subset of T st
( V in F & V c= S ) ) );

end;

:: deftheorem Def1 defines -quasi_basis YELLOW_8:def 1 :

registration

let T be non empty TopStruct ;
let x be Point of T;

cluster open x -quasi_basis for Element of bool (bool the carrier of T);

existence

proof end;

end;

theorem Th12: :: YELLOW_8:12

for T being non empty TopStruct
for x being Point of T
for B being Basis of x
for V being Subset of T st V in B holds
( V is open & x in V )

proof end;

theorem :: YELLOW_8:13

for T being non empty TopStruct
for x being Point of T
for B being Basis of x
for V being Subset of T st x in V & V is open holds
ex W being Subset of T st
( W in B & W c= V ) by Def1;

theorem :: YELLOW_8:14

for T being non empty TopStruct
for P being Subset-Family of T st P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) holds
P is Basis of T

proof end;

definition

let T be non empty TopSpace;

attr T is Baire means :: YELLOW_8:def 2
for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is everywhere_dense ) holds
ex I being Subset of T st
( I = Intersect F & I is dense );

end;

:: deftheorem defines Baire YELLOW_8:def 2 :

theorem :: YELLOW_8:15

for T being non empty TopSpace holds
( T is Baire iff for F being Subset-Family of T st F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) holds
union F is boundary )

proof end;

definition

let T be TopStruct ;
let S be Subset of T;

attr S is irreducible means :Def3: :: YELLOW_8:def 3
( not S is empty & S is closed & ( for S1, S2 being Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S ) );

end;

:: deftheorem Def3 defines irreducible YELLOW_8:def 3 :

registration

let T be TopStruct ;

cluster irreducible -> non empty for Element of bool the carrier of T;

coherence ;

end;

definition

let T be non empty TopSpace;
let S be Subset of T;
let p be Point of T;

pred p is_dense_point_of S means :: YELLOW_8:def 4
( p in S & S c= Cl {p} );

end;

:: deftheorem defines is_dense_point_of YELLOW_8:def 4 :

theorem :: YELLOW_8:16

for T being non empty TopSpace
for S being Subset of T st S is closed holds
for p being Point of T st p is_dense_point_of S holds
S = Cl {p} by ZFMISC_1:31, TOPS_1:5;

theorem Th17: :: YELLOW_8:17

for T being non empty TopSpace
for p being Point of T holds Cl {p} is irreducible

proof end;

registration

let T be non empty TopSpace;

cluster irreducible for Element of bool the carrier of T;

existence

proof end;

end;

definition

let T be non empty TopSpace;

attr T is sober means :Def5: :: YELLOW_8:def 5
for S being irreducible Subset of T ex p being Point of T st
( p is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds
p = q ) );

end;

:: deftheorem Def5 defines sober YELLOW_8:def 5 :

theorem Th18: :: YELLOW_8:18

for T being non empty TopSpace
for p being Point of T holds p is_dense_point_of Cl {p}

proof end;

theorem Th20: :: YELLOW_8:20

for T being non empty TopSpace
for G, F being Subset of T st G is open & F is closed holds
F \ G is closed

proof end;

theorem Th21: :: YELLOW_8:21

for T being non empty Hausdorff TopSpace
for S being irreducible Subset of T holds S is trivial

proof end;

registration

let T be non empty Hausdorff TopSpace;

cluster irreducible -> trivial for Element of bool the carrier of T;

coherence by Th21;

end;

registration

cluster non empty TopSpace-like Hausdorff -> non empty sober for TopStruct ;

coherence by Th22;

end;

registration

cluster non empty TopSpace-like sober for TopStruct ;

existence

proof end;

end;

theorem Th23: :: YELLOW_8:23

for T being non empty TopSpace holds
( T is T_0 iff for p, q being Point of T st Cl {p} = Cl {q} holds
p = q )

proof end;

registration

cluster non empty TopSpace-like sober -> non empty T_0 for TopStruct ;

coherence by Th24;

end;

definition

let X be set ;

func CofinTop X -> strict TopStruct means :Def6: :: YELLOW_8:def 6
( the carrier of it = X & COMPLEMENT the topology of it = {X} \/ (Fin X) );

existence

proof end;

uniqueness by SETFAM_1:38;

end;

:: deftheorem Def6 defines CofinTop YELLOW_8:def 6 :

registration

let X be non empty set ;

cluster CofinTop X -> non empty strict ;

coherence by Def6;

end;

theorem Th25: :: YELLOW_8:25

for X being non empty set
for P being Subset of (CofinTop X) holds
( P is closed iff ( P = X or P is finite ) )

proof end;

theorem Th26: :: YELLOW_8:26

for T being non empty TopSpace st T is T_1 holds
for p being Point of T holds Cl {p} = {p} by URYSOHN1:19, TOPS_1:5, PRE_TOPC:18;

registration

let X be non empty set ;

cluster CofinTop X -> strict T_1 ;

coherence

proof end;

end;

registration

let X be infinite set ;

cluster CofinTop X -> strict non sober ;

coherence

proof end;

end;

registration

cluster non empty TopSpace-like T_1 non sober for TopStruct ;

existence

proof end;

end;

theorem Th27: :: YELLOW_8:27

for T being non empty TopSpace holds
( T is regular iff for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Subset of T st
( Q is closed & Q c= P & p in Int Q ) )

proof end;

theorem :: YELLOW_8:28

for T being non empty TopSpace st T is regular holds
( T is locally-compact iff for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) )

proof end;