:: by Andrzej Trybulec

::

:: Received January 8, 1997

:: Copyright (c) 1997-2012 Association of Mizar Users

begin

begin

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 )

for F being Subset-Family of X

for P being Subset of X holds

( P ` in COMPLEMENT F iff P in F )

proof end;

begin

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

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

proof end;

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 ) }

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 :: 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 ) }

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;

begin

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

for T being non empty TopStruct

for x being Point of T

for F being Subset-Family of T holds

( F is x -quasi_basis iff ( 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 ) ) ) );

for T being non empty TopStruct

for x being Point of T

for F being Subset-Family of T holds

( F is x -quasi_basis iff ( 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 ) ) ) );

registration

let T be non empty TopStruct ;

let x be Point of T;

existence

ex b_{1} being Subset-Family of T st

( b_{1} is open & b_{1} is x -quasi_basis )

end;
let x be Point of T;

existence

ex b

( b

proof end;

definition

let T be non empty TopStruct ;

let x be Point of T;

mode Basis of x is open x -quasi_basis Subset-Family of T;

end;
let x be Point of T;

mode Basis of x is open x -quasi_basis Subset-Family of T;

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 )

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

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

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;

end;
attr T is Baire means :Def2: :: 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 );

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 );

:: deftheorem Def2 defines Baire YELLOW_8:def 2 :

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 everywhere_dense ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) );

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 everywhere_dense ) holds

ex I being Subset of T st

( I = Intersect F & I is dense ) );

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 )

( 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;

begin

:: deftheorem Def3 defines irreducible YELLOW_8:def 3 :

for T being TopStruct

for S being Subset of T holds

( S is irreducible iff ( 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 ) ) );

for T being TopStruct

for S being Subset of T holds

( S is irreducible iff ( 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 ) ) );

registration

let T be TopStruct ;

coherence

for b_{1} being Subset of T st b_{1} is irreducible holds

not b_{1} is empty
by Def3;

end;
coherence

for b

not b

:: deftheorem Def4 defines is_dense_point_of YELLOW_8:def 4 :

for T being non empty TopSpace

for S being Subset of T

for p being Point of T holds

( p is_dense_point_of S iff ( p in S & S c= Cl {p} ) );

for T being non empty TopSpace

for S being Subset of T

for p being Point of T holds

( p is_dense_point_of S iff ( p in S & S c= Cl {p} ) );

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}

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}

proof end;

registration

let T be non empty TopSpace;

existence

ex b_{1} being Subset of T st b_{1} is irreducible

end;
existence

ex b

proof end;

definition

let T be non empty TopSpace;

end;
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 ) );

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 ) );

:: deftheorem Def5 defines sober YELLOW_8:def 5 :

for T being non empty TopSpace holds

( T is sober iff 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 ) ) );

for T being non empty TopSpace holds

( T is sober iff 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 ) ) );

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

for G, F being Subset of T st G is open & F is closed holds

F \ G is closed

proof end;

registration

let T be non empty Hausdorff TopSpace;

coherence

for b_{1} being Subset of T st b_{1} is irreducible holds

b_{1} is trivial
by Th21;

end;
coherence

for b

b

registration
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 )

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

p = q )

proof end;

registration
end;

definition

let X be set ;

ex b_{1} being strict TopStruct st

( the carrier of b_{1} = X & COMPLEMENT the topology of b_{1} = {X} \/ (Fin X) )

for b_{1}, b_{2} being strict TopStruct st the carrier of b_{1} = X & COMPLEMENT the topology of b_{1} = {X} \/ (Fin X) & the carrier of b_{2} = X & COMPLEMENT the topology of b_{2} = {X} \/ (Fin X) holds

b_{1} = b_{2}
by SETFAM_1:38;

end;
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 ( the carrier of it = X & COMPLEMENT the topology of it = {X} \/ (Fin X) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def6 defines CofinTop YELLOW_8:def 6 :

for X being set

for b_{2} being strict TopStruct holds

( b_{2} = CofinTop X iff ( the carrier of b_{2} = X & COMPLEMENT the topology of b_{2} = {X} \/ (Fin X) ) );

for X being set

for b

( b

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 ) )

for P being Subset of (CofinTop X) holds

( P is closed iff ( P = X or P is finite ) )

proof end;

registration
end;

registration
end;

begin

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 ) )

( 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 ) )

( 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;