:: YELLOW_8 semantic presentation
begin
theorem Th1: :: YELLOW_8:1
for X, A, B being set st A in Fin X & B c= A holds
B in Fin X
proof
let X, A, B be set ; ::_thesis: ( A in Fin X & B c= A implies B in Fin X )
assume that
A1: A in Fin X and
A2: B c= A ; ::_thesis: B in Fin X
A c= X by A1, FINSUB_1:def_5;
then B c= X by A2, XBOOLE_1:1;
hence B in Fin X by A1, A2, FINSUB_1:def_5; ::_thesis: verum
end;
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
let X be set ; ::_thesis: for F being Subset-Family of X st F c= Fin X holds
meet F in Fin X
let F be Subset-Family of X; ::_thesis: ( F c= Fin X implies meet F in Fin X )
assume A1: F c= Fin X ; ::_thesis: meet F in Fin X
percases ( F = {} or F <> {} ) ;
suppose F = {} ; ::_thesis: meet F in Fin X
hence meet F in Fin X by FINSUB_1:7, SETFAM_1:1; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet F in Fin X
then consider A being set such that
A2: A in F by XBOOLE_0:def_1;
meet F c= A by A2, SETFAM_1:3;
hence meet F in Fin X by A1, A2, Th1; ::_thesis: verum
end;
end;
end;
begin
theorem Th3: :: YELLOW_8:3
for X being set
for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent
proof
let X be set ; ::_thesis: for F being Subset-Family of X holds F, COMPLEMENT F are_equipotent
let F be Subset-Family of X; ::_thesis: F, COMPLEMENT F are_equipotent
deffunc H1( set ) -> Element of bool X = X \ $1;
consider f being Function such that
A1: dom f = F and
A2: for x being set st x in F holds
f . x = H1(x) from FUNCT_1:sch_3();
take f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = F & rng f = COMPLEMENT F )
thus f is one-to-one ::_thesis: ( dom f = F & rng f = COMPLEMENT F )
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom f or not x2 in dom f or not f . x1 = f . x2 or x1 = x2 )
assume that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f . x1 = f . x2 ; ::_thesis: x1 = x2
reconsider X1 = x1, X2 = x2 as Subset of X by A1, A3, A4;
X1 ` = f . x1 by A1, A2, A3
.= X2 ` by A1, A2, A4, A5 ;
hence x1 = (X2 `) `
.= x2 ;
::_thesis: verum
end;
thus dom f = F by A1; ::_thesis: rng f = COMPLEMENT F
thus rng f c= COMPLEMENT F :: according to XBOOLE_0:def_10 ::_thesis: COMPLEMENT F c= rng f
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in rng f or e in COMPLEMENT F )
assume e in rng f ; ::_thesis: e in COMPLEMENT F
then consider u being set such that
A6: u in dom f and
A7: e = f . u by FUNCT_1:def_3;
reconsider Y = u as Subset of X by A1, A6;
e = Y ` by A1, A2, A6, A7;
hence e in COMPLEMENT F by A1, A6, SETFAM_1:35; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in COMPLEMENT F or e in rng f )
assume A8: e in COMPLEMENT F ; ::_thesis: e in rng f
then reconsider Y = e as Subset of X ;
A9: Y ` in F by A8, SETFAM_1:def_7;
e = (Y `) `
.= f . (Y `) by A2, A9 ;
hence e in rng f by A1, A9, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th4: :: YELLOW_8:4
for X, Y being set st X,Y are_equipotent & X is countable holds
Y is countable
proof
let X, Y be set ; ::_thesis: ( X,Y are_equipotent & X is countable implies Y is countable )
assume ( X,Y are_equipotent & card X c= omega ) ; :: according to CARD_3:def_14 ::_thesis: Y is countable
hence card Y c= omega by CARD_1:5; :: according to CARD_3:def_14 ::_thesis: verum
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
let X be 1-sorted ; ::_thesis: for F being Subset-Family of X
for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
let F be Subset-Family of X; ::_thesis: for P being Subset of X holds
( P ` in COMPLEMENT F iff P in F )
let P be Subset of X; ::_thesis: ( P ` in COMPLEMENT F iff P in F )
P = (P `) ` ;
hence ( P ` in COMPLEMENT F iff P in F ) by SETFAM_1:def_7; ::_thesis: verum
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
let X be 1-sorted ; ::_thesis: for F being Subset-Family of X holds Intersect (COMPLEMENT F) = (union F) `
let F be Subset-Family of X; ::_thesis: Intersect (COMPLEMENT F) = (union F) `
percases ( F <> {} or F = {} ) ;
supposeA1: F <> {} ; ::_thesis: Intersect (COMPLEMENT F) = (union F) `
then COMPLEMENT F <> {} by SETFAM_1:32;
hence Intersect (COMPLEMENT F) = meet (COMPLEMENT F) by SETFAM_1:def_9
.= ([#] the carrier of X) \ (union F) by A1, SETFAM_1:33
.= (union F) ` ;
::_thesis: verum
end;
suppose F = {} ; ::_thesis: Intersect (COMPLEMENT F) = (union F) `
then reconsider G = F as empty Subset-Family of X ;
COMPLEMENT G = {} ;
hence Intersect (COMPLEMENT F) = (union F) ` by SETFAM_1:def_9, ZFMISC_1:2; ::_thesis: verum
end;
end;
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
let X be 1-sorted ; ::_thesis: for F being Subset-Family of X holds union (COMPLEMENT F) = (Intersect F) `
let F be Subset-Family of X; ::_thesis: union (COMPLEMENT F) = (Intersect F) `
thus union (COMPLEMENT F) = ((union (COMPLEMENT F)) `) `
.= (Intersect (COMPLEMENT (COMPLEMENT F))) ` by Th6
.= (Intersect F) ` ; ::_thesis: verum
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
proof
let T be non empty TopSpace; ::_thesis: 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
let A, B be Subset of T; ::_thesis: ( B c= A & A is closed & ( for C being Subset of T st B c= C & C is closed holds
A c= C ) implies A = Cl B )
assume that
A1: ( B c= A & A is closed ) and
A2: for C being Subset of T st B c= C & C is closed holds
A c= C ; ::_thesis: A = Cl B
thus A c= Cl B by A2, PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl B c= A
thus Cl B c= A by A1, TOPS_1:5; ::_thesis: verum
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 ) }
proof
let T be TopStruct ; ::_thesis: 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 ) }
let B be Basis of T; ::_thesis: 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 ) }
let V be Subset of T; ::_thesis: ( V is open implies V = union { G where G is Subset of T : ( G in B & G c= V ) } )
assume A1: V is open ; ::_thesis: V = union { G where G is Subset of T : ( G in B & G c= V ) }
set X = { G where G is Subset of T : ( G in B & G c= V ) } ;
A2: the topology of T c= UniCl B by CANTOR_1:def_2;
for x being set holds
( x in V iff ex Y being set st
( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) )
proof
let x be set ; ::_thesis: ( x in V iff ex Y being set st
( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) )
hereby ::_thesis: ( ex Y being set st
( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) implies x in V )
V in the topology of T by A1, PRE_TOPC:def_2;
then consider Y being Subset-Family of T such that
A3: Y c= B and
A4: V = union Y by A2, CANTOR_1:def_1;
assume x in V ; ::_thesis: ex W being set st
( x in W & W in { G where G is Subset of T : ( G in B & G c= V ) } )
then consider W being set such that
A5: x in W and
A6: W in Y by A4, TARSKI:def_4;
take W = W; ::_thesis: ( x in W & W in { G where G is Subset of T : ( G in B & G c= V ) } )
thus x in W by A5; ::_thesis: W in { G where G is Subset of T : ( G in B & G c= V ) }
reconsider G = W as Subset of T by A6;
G c= V by A4, A6, ZFMISC_1:74;
hence W in { G where G is Subset of T : ( G in B & G c= V ) } by A3, A6; ::_thesis: verum
end;
given Y being set such that A7: x in Y and
A8: Y in { G where G is Subset of T : ( G in B & G c= V ) } ; ::_thesis: x in V
ex G being Subset of T st
( Y = G & G in B & G c= V ) by A8;
hence x in V by A7; ::_thesis: verum
end;
hence V = union { G where G is Subset of T : ( G in B & G c= V ) } by TARSKI:def_4; ::_thesis: verum
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
let T be TopStruct ; ::_thesis: for B being Basis of T
for S being Subset of T st S in B holds
S is open
let B be Basis of T; ::_thesis: for S being Subset of T st S in B holds
S is open
let S be Subset of T; ::_thesis: ( S in B implies S is open )
assume A1: S in B ; ::_thesis: S is open
B c= the topology of T by TOPS_2:64;
hence S is open by A1, PRE_TOPC:def_2; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: 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 ) }
let B be Basis of T; ::_thesis: for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }
let V be Subset of T; ::_thesis: Int V = union { G where G is Subset of T : ( G in B & G c= V ) }
set X = { G where G is Subset of T : ( G in B & G c= V ) } ;
set Y = { G where G is Subset of T : ( G in B & G c= Int V ) } ;
{ G where G is Subset of T : ( G in B & G c= V ) } = { G where G is Subset of T : ( G in B & G c= Int V ) }
proof
thus { G where G is Subset of T : ( G in B & G c= V ) } c= { G where G is Subset of T : ( G in B & G c= Int V ) } :: according to XBOOLE_0:def_10 ::_thesis: { G where G is Subset of T : ( G in B & G c= Int V ) } c= { G where G is Subset of T : ( G in B & G c= V ) }
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { G where G is Subset of T : ( G in B & G c= V ) } or e in { G where G is Subset of T : ( G in B & G c= Int V ) } )
assume e in { G where G is Subset of T : ( G in B & G c= V ) } ; ::_thesis: e in { G where G is Subset of T : ( G in B & G c= Int V ) }
then consider G being Subset of T such that
A1: e = G and
A2: G in B and
A3: G c= V ;
G c= Int V by A2, A3, Th10, TOPS_1:24;
hence e in { G where G is Subset of T : ( G in B & G c= Int V ) } by A1, A2; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { G where G is Subset of T : ( G in B & G c= Int V ) } or e in { G where G is Subset of T : ( G in B & G c= V ) } )
assume e in { G where G is Subset of T : ( G in B & G c= Int V ) } ; ::_thesis: e in { G where G is Subset of T : ( G in B & G c= V ) }
then consider G being Subset of T such that
A4: ( e = G & G in B ) and
A5: G c= Int V ;
Int V c= V by TOPS_1:16;
then G c= V by A5, XBOOLE_1:1;
hence e in { G where G is Subset of T : ( G in B & G c= V ) } by A4; ::_thesis: verum
end;
hence Int V = union { G where G is Subset of T : ( G in B & G c= V ) } by Th9; ::_thesis: verum
end;
begin
definition
let T be non empty TopStruct ;
let x be Point of T;
let F be Subset-Family of T;
attrF 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_:_
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;
cluster open x -quasi_basis for Element of bool (bool the carrier of T);
existence
ex b1 being Subset-Family of T st
( b1 is open & b1 is x -quasi_basis )
proof
defpred S1[ set ] means ( T in the topology of T & x in T );
set IT = { S where S is Subset of T : S1[S] } ;
{ S where S is Subset of T : S1[S] } is Subset-Family of T from DOMAIN_1:sch_7();
then reconsider IT = { S where S is Subset of T : S1[S] } as Subset-Family of T ;
take IT ; ::_thesis: ( IT is open & IT is x -quasi_basis )
IT c= the topology of T
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in IT or e in the topology of T )
assume e in IT ; ::_thesis: e in the topology of T
then ex S being Subset of T st
( S = e & S in the topology of T & x in S ) ;
hence e in the topology of T ; ::_thesis: verum
end;
hence IT is open by TOPS_2:64; ::_thesis: IT is x -quasi_basis
now__::_thesis:_for_e_being_set_st_e_in_IT_holds_
x_in_e
let e be set ; ::_thesis: ( e in IT implies x in e )
assume e in IT ; ::_thesis: x in e
then ex S being Subset of T st
( S = e & S in the topology of T & x in S ) ;
hence x in e ; ::_thesis: verum
end;
hence x in Intersect IT by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for S being Subset of T st S is open & x in S holds
ex V being Subset of T st
( V in IT & V c= S )
let S be Subset of T; ::_thesis: ( S is open & x in S implies ex V being Subset of T st
( V in IT & V c= S ) )
assume that
A1: S is open and
A2: x in S ; ::_thesis: ex V being Subset of T st
( V in IT & V c= S )
take V = S; ::_thesis: ( V in IT & V c= S )
V in the topology of T by A1, PRE_TOPC:def_2;
hence V in IT by A2; ::_thesis: V c= S
thus V c= S ; ::_thesis: verum
end;
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;
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
let T be non empty TopStruct ; ::_thesis: 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 )
let x be Point of T; ::_thesis: for B being Basis of x
for V being Subset of T st V in B holds
( V is open & x in V )
let B be Basis of x; ::_thesis: for V being Subset of T st V in B holds
( V is open & x in V )
let V be Subset of T; ::_thesis: ( V in B implies ( V is open & x in V ) )
assume A1: V in B ; ::_thesis: ( V is open & x in V )
B c= the topology of T by TOPS_2:64;
hence V is open by A1, PRE_TOPC:def_2; ::_thesis: x in V
x in Intersect B by Def1;
hence x in V by A1, SETFAM_1:43; ::_thesis: verum
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
let T be non empty TopStruct ; ::_thesis: 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
let P be Subset-Family of T; ::_thesis: ( P c= the topology of T & ( for x being Point of T ex B being Basis of x st B c= P ) implies P is Basis of T )
assume that
A1: P c= the topology of T and
A2: for x being Point of T ex B being Basis of x st B c= P ; ::_thesis: P is Basis of T
P is quasi_basis
proof
let e be set ; :: according to TARSKI:def_3,CANTOR_1:def_2 ::_thesis: ( not e in the topology of T or e in UniCl P )
assume A3: e in the topology of T ; ::_thesis: e in UniCl P
then reconsider S = e as Subset of T ;
set X = { V where V is Subset of T : ( V in P & V c= S ) } ;
A4: { V where V is Subset of T : ( V in P & V c= S ) } c= P
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { V where V is Subset of T : ( V in P & V c= S ) } or e in P )
assume e in { V where V is Subset of T : ( V in P & V c= S ) } ; ::_thesis: e in P
then ex V being Subset of T st
( e = V & V in P & V c= S ) ;
hence e in P ; ::_thesis: verum
end;
then reconsider X = { V where V is Subset of T : ( V in P & V c= S ) } as Subset-Family of T by XBOOLE_1:1;
for u being set holds
( u in S iff ex Z being set st
( u in Z & Z in X ) )
proof
let u be set ; ::_thesis: ( u in S iff ex Z being set st
( u in Z & Z in X ) )
hereby ::_thesis: ( ex Z being set st
( u in Z & Z in X ) implies u in S )
assume A5: u in S ; ::_thesis: ex Z being set st
( u in Z & Z in X )
then reconsider p = u as Point of T ;
consider B being Basis of p such that
A6: B c= P by A2;
S is open by A3, PRE_TOPC:def_2;
then consider W being Subset of T such that
A7: W in B and
A8: W c= S by A5, Def1;
reconsider Z = W as set ;
take Z = Z; ::_thesis: ( u in Z & Z in X )
thus u in Z by A7, Th12; ::_thesis: Z in X
thus Z in X by A6, A7, A8; ::_thesis: verum
end;
given Z being set such that A9: u in Z and
A10: Z in X ; ::_thesis: u in S
ex V being Subset of T st
( V = Z & V in P & V c= S ) by A10;
hence u in S by A9; ::_thesis: verum
end;
then S = union X by TARSKI:def_4;
hence e in UniCl P by A4, CANTOR_1:def_1; ::_thesis: verum
end;
hence P is Basis of T by A1, TOPS_2:64; ::_thesis: verum
end;
definition
let T be non empty TopSpace;
attrT 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 );
end;
:: 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 ) );
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
let T be non empty TopSpace; ::_thesis: ( 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 )
hereby ::_thesis: ( ( 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 ) implies T is Baire )
assume A1: T is Baire ; ::_thesis: 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
let F be Subset-Family of T; ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds
S is nowhere_dense ) implies union F is boundary )
assume that
A2: F is countable and
A3: for S being Subset of T st S in F holds
S is nowhere_dense ; ::_thesis: union F is boundary
reconsider G = COMPLEMENT F as Subset-Family of T ;
A4: for S being Subset of T st S in G holds
S is everywhere_dense
proof
let S be Subset of T; ::_thesis: ( S in G implies S is everywhere_dense )
assume S in G ; ::_thesis: S is everywhere_dense
then S ` in F by SETFAM_1:def_7;
then S ` is nowhere_dense by A3;
hence S is everywhere_dense by TOPS_3:39; ::_thesis: verum
end;
G is countable by A2, Th3, Th4;
then ex I being Subset of T st
( I = Intersect G & I is dense ) by A1, A4, Def2;
then (union F) ` is dense by Th6;
hence union F is boundary by TOPS_1:def_4; ::_thesis: verum
end;
assume A5: 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 ; ::_thesis: T is Baire
let F be Subset-Family of T; :: according to YELLOW_8:def_2 ::_thesis: ( F is countable & ( for S being Subset of T st S in F holds
S is everywhere_dense ) implies ex I being Subset of T st
( I = Intersect F & I is dense ) )
assume that
A6: F is countable and
A7: for S being Subset of T st S in F holds
S is everywhere_dense ; ::_thesis: ex I being Subset of T st
( I = Intersect F & I is dense )
reconsider I = Intersect F as Subset of T ;
take I ; ::_thesis: ( I = Intersect F & I is dense )
thus I = Intersect F ; ::_thesis: I is dense
reconsider G = COMPLEMENT F as Subset-Family of T ;
A8: for S being Subset of T st S in G holds
S is nowhere_dense
proof
let S be Subset of T; ::_thesis: ( S in G implies S is nowhere_dense )
assume S in G ; ::_thesis: S is nowhere_dense
then S ` in F by SETFAM_1:def_7;
then S ` is everywhere_dense by A7;
hence S is nowhere_dense by TOPS_3:40; ::_thesis: verum
end;
G is countable by A6, Th3, Th4;
then union G is boundary by A5, A8;
then (Intersect F) ` is boundary by Th7;
hence I is dense by TOPS_3:18; ::_thesis: verum
end;
begin
definition
let T be TopStruct ;
let S be Subset of T;
attrS 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_:_
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 ;
cluster irreducible -> non empty for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is irreducible holds
not b1 is empty by Def3;
end;
definition
let T be non empty TopSpace;
let S be Subset of T;
let p be Point of T;
predp is_dense_point_of S means :Def4: :: YELLOW_8:def 4
( p in S & S c= Cl {p} );
end;
:: 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} ) );
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}
proof
let T be non empty TopSpace; ::_thesis: 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}
let S be Subset of T; ::_thesis: ( S is closed implies for p being Point of T st p is_dense_point_of S holds
S = Cl {p} )
assume A1: S is closed ; ::_thesis: for p being Point of T st p is_dense_point_of S holds
S = Cl {p}
let p be Point of T; ::_thesis: ( p is_dense_point_of S implies S = Cl {p} )
assume that
A2: p in S and
A3: S c= Cl {p} ; :: according to YELLOW_8:def_4 ::_thesis: S = Cl {p}
{p} c= S by A2, ZFMISC_1:31;
then Cl {p} c= S by A1, TOPS_1:5;
hence S = Cl {p} by A3, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th17: :: YELLOW_8:17
for T being non empty TopSpace
for p being Point of T holds Cl {p} is irreducible
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds Cl {p} is irreducible
let p be Point of T; ::_thesis: Cl {p} is irreducible
assume A1: not Cl {p} is irreducible ; ::_thesis: contradiction
not Cl {p} is empty by PCOMPS_1:2;
then consider S1, S2 being Subset of T such that
A2: ( S1 is closed & S2 is closed ) and
A3: Cl {p} = S1 \/ S2 and
A4: ( S1 <> Cl {p} & S2 <> Cl {p} ) by A1, Def3;
( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def_1;
then ( p in S1 or p in S2 ) by A3, XBOOLE_0:def_3;
then ( {p} c= S1 or {p} c= S2 ) by ZFMISC_1:31;
then A5: ( Cl {p} c= S1 or Cl {p} c= S2 ) by A2, TOPS_1:5;
( S1 c= Cl {p} & S2 c= Cl {p} ) by A3, XBOOLE_1:7;
hence contradiction by A4, A5, XBOOLE_0:def_10; ::_thesis: verum
end;
registration
let T be non empty TopSpace;
cluster irreducible for Element of bool the carrier of T;
existence
ex b1 being Subset of T st b1 is irreducible
proof
set p = the Point of T;
Cl { the Point of T} is irreducible by Th17;
hence ex b1 being Subset of T st b1 is irreducible ; ::_thesis: verum
end;
end;
definition
let T be non empty TopSpace;
attrT 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_:_
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 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
let T be non empty TopSpace; ::_thesis: for p being Point of T holds p is_dense_point_of Cl {p}
let p be Point of T; ::_thesis: p is_dense_point_of Cl {p}
( {p} c= Cl {p} & p in {p} ) by PRE_TOPC:18, TARSKI:def_1;
hence p in Cl {p} ; :: according to YELLOW_8:def_4 ::_thesis: Cl {p} c= Cl {p}
thus Cl {p} c= Cl {p} ; ::_thesis: verum
end;
theorem Th19: :: YELLOW_8:19
for T being non empty TopSpace
for p being Point of T holds p is_dense_point_of {p}
proof
let T be non empty TopSpace; ::_thesis: for p being Point of T holds p is_dense_point_of {p}
let p be Point of T; ::_thesis: p is_dense_point_of {p}
thus p in {p} by TARSKI:def_1; :: according to YELLOW_8:def_4 ::_thesis: {p} c= Cl {p}
thus {p} c= Cl {p} by PRE_TOPC:18; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: for G, F being Subset of T st G is open & F is closed holds
F \ G is closed
let G, F be Subset of T; ::_thesis: ( G is open & F is closed implies F \ G is closed )
assume A1: ( G is open & F is closed ) ; ::_thesis: F \ G is closed
F \ G = F /\ (G `) by SUBSET_1:13;
hence F \ G is closed by A1; ::_thesis: verum
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
let T be non empty Hausdorff TopSpace; ::_thesis: for S being irreducible Subset of T holds S is trivial
let S be irreducible Subset of T; ::_thesis: S is trivial
assume not S is trivial ; ::_thesis: contradiction
then consider x, y being Point of T such that
A1: ( x in S & y in S ) and
A2: x <> y by SUBSET_1:45;
consider W, V being Subset of T such that
A3: ( W is open & V is open ) and
A4: ( x in W & y in V ) and
A5: W misses V by A2, PRE_TOPC:def_10;
set S1 = S \ W;
set S2 = S \ V;
A6: ( S \ W <> S & S \ V <> S ) by A4, A1, XBOOLE_0:def_5;
S is closed by Def3;
then A7: ( S \ W is closed & S \ V is closed ) by A3, Th20;
A8: W /\ V = {} by A5, XBOOLE_0:def_7;
(S \ W) \/ (S \ V) = S \ (W /\ V) by XBOOLE_1:54
.= S by A8 ;
hence contradiction by A7, A6, Def3; ::_thesis: verum
end;
registration
let T be non empty Hausdorff TopSpace;
cluster irreducible -> trivial for Element of bool the carrier of T;
coherence
for b1 being Subset of T st b1 is irreducible holds
b1 is trivial by Th21;
end;
theorem Th22: :: YELLOW_8:22
for T being non empty Hausdorff TopSpace holds T is sober
proof
let T be non empty Hausdorff TopSpace; ::_thesis: T is sober
let S be irreducible Subset of T; :: according to YELLOW_8:def_5 ::_thesis: 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 ) )
consider d being Element of S such that
A1: S = {d} by SUBSET_1:46;
reconsider d = d as Point of T ;
take d ; ::_thesis: ( d is_dense_point_of S & ( for q being Point of T st q is_dense_point_of S holds
d = q ) )
thus d is_dense_point_of S by A1, Th19; ::_thesis: for q being Point of T st q is_dense_point_of S holds
d = q
let p be Point of T; ::_thesis: ( p is_dense_point_of S implies d = p )
assume p is_dense_point_of S ; ::_thesis: d = p
then p in S by Def4;
hence d = p by A1, TARSKI:def_1; ::_thesis: verum
end;
registration
cluster non empty TopSpace-like Hausdorff -> non empty sober for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is Hausdorff holds
b1 is sober by Th22;
end;
registration
cluster non empty TopSpace-like sober for TopStruct ;
existence
ex b1 being non empty TopSpace st b1 is sober
proof
set T = the non empty Hausdorff TopSpace;
take the non empty Hausdorff TopSpace ; ::_thesis: the non empty Hausdorff TopSpace is sober
thus the non empty Hausdorff TopSpace is sober ; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: ( T is T_0 iff for p, q being Point of T st Cl {p} = Cl {q} holds
p = q )
thus ( T is T_0 implies for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ) by TSP_1:def_5; ::_thesis: ( ( for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ) implies T is T_0 )
assume for p, q being Point of T st Cl {p} = Cl {q} holds
p = q ; ::_thesis: T is T_0
then for p, q being Point of T st p <> q holds
Cl {p} <> Cl {q} ;
hence T is T_0 by TSP_1:def_5; ::_thesis: verum
end;
theorem Th24: :: YELLOW_8:24
for T being non empty sober TopSpace holds T is T_0
proof
let T be non empty sober TopSpace; ::_thesis: T is T_0
for p, q being Point of T st Cl {p} = Cl {q} holds
p = q
proof
let p, q be Point of T; ::_thesis: ( Cl {p} = Cl {q} implies p = q )
assume A1: Cl {p} = Cl {q} ; ::_thesis: p = q
Cl {p} is irreducible by Th17;
then consider r being Point of T such that
r is_dense_point_of Cl {p} and
A2: for q being Point of T st q is_dense_point_of Cl {p} holds
r = q by Def5;
p = r by A2, Th18;
hence p = q by A1, A2, Th18; ::_thesis: verum
end;
hence T is T_0 by Th23; ::_thesis: verum
end;
registration
cluster non empty TopSpace-like sober -> non empty T_0 for TopStruct ;
coherence
for b1 being non empty TopSpace st b1 is sober holds
b1 is T_0 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
ex b1 being strict TopStruct st
( the carrier of b1 = X & COMPLEMENT the topology of b1 = {X} \/ (Fin X) )
proof
( {X} c= bool X & Fin X c= bool X ) by FINSUB_1:13, ZFMISC_1:68;
then reconsider F = {X} \/ (Fin X) as Subset-Family of X by XBOOLE_1:8;
reconsider F = F as Subset-Family of X ;
take T = TopStruct(# X,(COMPLEMENT F) #); ::_thesis: ( the carrier of T = X & COMPLEMENT the topology of T = {X} \/ (Fin X) )
thus the carrier of T = X ; ::_thesis: COMPLEMENT the topology of T = {X} \/ (Fin X)
thus COMPLEMENT the topology of T = {X} \/ (Fin X) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict TopStruct st the carrier of b1 = X & COMPLEMENT the topology of b1 = {X} \/ (Fin X) & the carrier of b2 = X & COMPLEMENT the topology of b2 = {X} \/ (Fin X) holds
b1 = b2 by SETFAM_1:38;
end;
:: deftheorem Def6 defines CofinTop YELLOW_8:def_6_:_
for X being set
for b2 being strict TopStruct holds
( b2 = CofinTop X iff ( the carrier of b2 = X & COMPLEMENT the topology of b2 = {X} \/ (Fin X) ) );
registration
let X be non empty set ;
cluster CofinTop X -> non empty strict ;
coherence
not CofinTop X is empty by Def6;
end;
registration
let X be set ;
cluster CofinTop X -> strict TopSpace-like ;
coherence
CofinTop X is TopSpace-like
proof
reconsider F = Fin X as Subset-Family of X by FINSUB_1:13;
reconsider XX = {X} as Subset-Family of X by ZFMISC_1:68;
set IT = CofinTop X;
reconsider XX = XX as Subset-Family of X ;
reconsider F = F as Subset-Family of X ;
A1: the carrier of (CofinTop X) = X by Def6;
A2: COMPLEMENT the topology of (CofinTop X) = {X} \/ (Fin X) by Def6;
A3: the topology of (CofinTop X) = COMPLEMENT (COMPLEMENT the topology of (CofinTop X))
.= (COMPLEMENT XX) \/ (COMPLEMENT F) by A1, A2, SETFAM_1:39
.= {{}} \/ (COMPLEMENT F) by SETFAM_1:40 ;
{}. X in F ;
then (({} X) `) ` in F ;
then [#] X in COMPLEMENT F by SETFAM_1:def_7;
hence the carrier of (CofinTop X) in the topology of (CofinTop X) by A1, A3, XBOOLE_0:def_3; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of (CofinTop X)) holds
( not b1 c= the topology of (CofinTop X) or union b1 in the topology of (CofinTop X) ) ) & ( for b1, b2 being Element of bool the carrier of (CofinTop X) holds
( not b1 in the topology of (CofinTop X) or not b2 in the topology of (CofinTop X) or b1 /\ b2 in the topology of (CofinTop X) ) ) )
A4: {} in {{}} by TARSKI:def_1;
thus for a being Subset-Family of (CofinTop X) st a c= the topology of (CofinTop X) holds
union a in the topology of (CofinTop X) ::_thesis: for b1, b2 being Element of bool the carrier of (CofinTop X) holds
( not b1 in the topology of (CofinTop X) or not b2 in the topology of (CofinTop X) or b1 /\ b2 in the topology of (CofinTop X) )
proof
let a be Subset-Family of (CofinTop X); ::_thesis: ( a c= the topology of (CofinTop X) implies union a in the topology of (CofinTop X) )
assume A5: a c= the topology of (CofinTop X) ; ::_thesis: union a in the topology of (CofinTop X)
set b = a /\ (COMPLEMENT F);
reconsider b = a /\ (COMPLEMENT F) as Subset-Family of X ;
reconsider b = b as Subset-Family of X ;
a /\ {{}} c= {{}} by XBOOLE_1:17;
then ( a /\ {{}} = {{}} or a /\ {{}} = {} ) by ZFMISC_1:33;
then A6: union (a /\ {{}}) = {} by ZFMISC_1:2, ZFMISC_1:25;
A7: union a = union (a /\ the topology of (CofinTop X)) by A5, XBOOLE_1:28
.= union ((a /\ {{}}) \/ (a /\ (COMPLEMENT F))) by A3, XBOOLE_1:23
.= (union (a /\ {{}})) \/ (union (a /\ (COMPLEMENT F))) by ZFMISC_1:78
.= union b by A6 ;
percases ( b = {} or b <> {} ) ;
suppose b = {} ; ::_thesis: union a in the topology of (CofinTop X)
hence union a in the topology of (CofinTop X) by A3, A4, A7, XBOOLE_0:def_3, ZFMISC_1:2; ::_thesis: verum
end;
supposeA8: b <> {} ; ::_thesis: union a in the topology of (CofinTop X)
b c= COMPLEMENT F by XBOOLE_1:17;
then A9: COMPLEMENT b c= Fin X by SETFAM_1:37;
meet (COMPLEMENT b) = ([#] X) \ (union b) by A8, SETFAM_1:33
.= (union b) ` ;
then (union b) ` in Fin X by A9, Th2;
then union b in COMPLEMENT F by SETFAM_1:def_7;
hence union a in the topology of (CofinTop X) by A3, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
let a, b be Subset of (CofinTop X); ::_thesis: ( not a in the topology of (CofinTop X) or not b in the topology of (CofinTop X) or a /\ b in the topology of (CofinTop X) )
assume that
A10: a in the topology of (CofinTop X) and
A11: b in the topology of (CofinTop X) ; ::_thesis: a /\ b in the topology of (CofinTop X)
reconsider a9 = a, b9 = b as Subset of X by Def6;
percases ( a = {} or b = {} or ( a <> {} & b <> {} ) ) ;
suppose ( a = {} or b = {} ) ; ::_thesis: a /\ b in the topology of (CofinTop X)
hence a /\ b in the topology of (CofinTop X) by A3, A4, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA12: ( a <> {} & b <> {} ) ; ::_thesis: a /\ b in the topology of (CofinTop X)
then not b in {{}} by TARSKI:def_1;
then b9 in COMPLEMENT F by A3, A11, XBOOLE_0:def_3;
then A13: b9 ` in Fin X by SETFAM_1:def_7;
not a in {{}} by A12, TARSKI:def_1;
then a9 in COMPLEMENT F by A3, A10, XBOOLE_0:def_3;
then a9 ` in Fin X by SETFAM_1:def_7;
then (a9 `) \/ (b9 `) in Fin X by A13, FINSUB_1:1;
then (a9 /\ b9) ` in Fin X by XBOOLE_1:54;
then a /\ b in COMPLEMENT F by SETFAM_1:def_7;
hence a /\ b in the topology of (CofinTop X) by A3, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
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
let X be non empty set ; ::_thesis: for P being Subset of (CofinTop X) holds
( P is closed iff ( P = X or P is finite ) )
let P be Subset of (CofinTop X); ::_thesis: ( P is closed iff ( P = X or P is finite ) )
set T = CofinTop X;
hereby ::_thesis: ( ( P = X or P is finite ) implies P is closed )
assume that
A1: P is closed and
A2: P <> X ; ::_thesis: P is finite
P ` in the topology of (CofinTop X) by A1, PRE_TOPC:def_2;
then P in COMPLEMENT the topology of (CofinTop X) by SETFAM_1:def_7;
then A3: P in {X} \/ (Fin X) by Def6;
not P in {X} by A2, TARSKI:def_1;
then P in Fin X by A3, XBOOLE_0:def_3;
hence P is finite ; ::_thesis: verum
end;
assume A4: ( P = X or P is finite ) ; ::_thesis: P is closed
the carrier of (CofinTop X) = X by Def6;
then ( P in {X} or P in Fin X ) by A4, FINSUB_1:def_5, TARSKI:def_1;
then P in {X} \/ (Fin X) by XBOOLE_0:def_3;
then P in COMPLEMENT the topology of (CofinTop X) by Def6;
then P ` in the topology of (CofinTop X) by SETFAM_1:def_7;
then P ` is open by PRE_TOPC:def_2;
hence P is closed by TOPS_1:3; ::_thesis: verum
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}
proof
let T be non empty TopSpace; ::_thesis: ( T is T_1 implies for p being Point of T holds Cl {p} = {p} )
assume A1: T is T_1 ; ::_thesis: for p being Point of T holds Cl {p} = {p}
let p be Point of T; ::_thesis: Cl {p} = {p}
{p} is closed by A1, URYSOHN1:19;
then A2: Cl {p} c= {p} by TOPS_1:5;
{p} c= Cl {p} by PRE_TOPC:18;
hence Cl {p} = {p} by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
registration
let X be non empty set ;
cluster CofinTop X -> strict T_1 ;
coherence
CofinTop X is T_1
proof
for p being Point of (CofinTop X) holds {p} is closed by Th25;
hence CofinTop X is T_1 by URYSOHN1:19; ::_thesis: verum
end;
end;
registration
let X be infinite set ;
cluster CofinTop X -> strict non sober ;
coherence
not CofinTop X is sober
proof
set T = CofinTop X;
reconsider S = [#] X as Subset of (CofinTop X) by Def6;
S is irreducible
proof
X = [#] (CofinTop X) by Def6;
hence ( not S is empty & S is closed ) ; :: according to YELLOW_8:def_3 ::_thesis: for S1, S2 being Subset of (CofinTop X) st S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S holds
S2 = S
let S1, S2 be Subset of (CofinTop X); ::_thesis: ( S1 is closed & S2 is closed & S = S1 \/ S2 & not S1 = S implies S2 = S )
assume that
A1: ( S1 is closed & S2 is closed ) and
A2: S = S1 \/ S2 ; ::_thesis: ( S1 = S or S2 = S )
assume ( S1 <> S & S2 <> S ) ; ::_thesis: contradiction
then reconsider S19 = S1, S29 = S2 as finite set by A1, Th25;
S = S19 \/ S29 by A2;
hence contradiction ; ::_thesis: verum
end;
then reconsider S = S as irreducible Subset of (CofinTop X) ;
take S ; :: according to YELLOW_8:def_5 ::_thesis: for p being Point of (CofinTop X) holds
( not p is_dense_point_of S or ex q being Point of (CofinTop X) st
( q is_dense_point_of S & not p = q ) )
let p be Point of (CofinTop X); ::_thesis: ( not p is_dense_point_of S or ex q being Point of (CofinTop X) st
( q is_dense_point_of S & not p = q ) )
now__::_thesis:_not_p_is_dense_point_of_S
assume p is_dense_point_of S ; ::_thesis: contradiction
then S c= Cl {p} by Def4;
then Cl {p} is infinite ;
hence contradiction by Th26; ::_thesis: verum
end;
hence ( not p is_dense_point_of S or ex q being Point of (CofinTop X) st
( q is_dense_point_of S & not p = q ) ) ; ::_thesis: verum
end;
end;
registration
cluster non empty TopSpace-like T_1 non sober for TopStruct ;
existence
ex b1 being non empty TopSpace st
( b1 is T_1 & not b1 is sober )
proof
set X = the infinite set ;
take CofinTop the infinite set ; ::_thesis: ( CofinTop the infinite set is T_1 & not CofinTop the infinite set is sober )
thus ( CofinTop the infinite set is T_1 & not CofinTop the infinite set is sober ) ; ::_thesis: verum
end;
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 ) )
proof
let T be non empty TopSpace; ::_thesis: ( 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 ) )
hereby ::_thesis: ( ( 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 ) ) implies T is regular )
assume A1: T is regular ; ::_thesis: for p being Point of T
for P being Subset of T st p in Int P holds
ex Q being Element of bool the carrier of T st
( b5 is closed & b5 c= b4 & Q in Int b5 )
let p be Point of T; ::_thesis: for P being Subset of T st p in Int P holds
ex Q being Element of bool the carrier of T st
( b4 is closed & b4 c= b3 & Q in Int b4 )
let P be Subset of T; ::_thesis: ( p in Int P implies ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 ) )
assume p in Int P ; ::_thesis: ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 )
then A2: p in ((Int P) `) ` ;
percases ( P = [#] T or P <> [#] T ) ;
supposeA3: P = [#] T ; ::_thesis: ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 )
take Q = [#] T; ::_thesis: ( Q is closed & Q c= P & p in Int Q )
thus Q is closed ; ::_thesis: ( Q c= P & p in Int Q )
thus Q c= P by A3; ::_thesis: p in Int Q
Int Q = Q by TOPS_1:15;
hence p in Int Q ; ::_thesis: verum
end;
supposeA4: P <> [#] T ; ::_thesis: ex Q being Element of bool the carrier of T st
( b3 is closed & b3 c= b2 & Q in Int b3 )
now__::_thesis:_not_(Int_P)_`_=_{}
assume (Int P) ` = {} ; ::_thesis: contradiction
then ((Int P) `) ` = [#] T ;
then [#] T c= P by TOPS_1:16;
hence contradiction by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
then consider W, V being Subset of T such that
A5: W is open and
A6: V is open and
A7: p in W and
A8: (Int P) ` c= V and
A9: W misses V by A1, A2, COMPTS_1:def_2;
A10: Int P c= P by TOPS_1:16;
take Q = V ` ; ::_thesis: ( Q is closed & Q c= P & p in Int Q )
thus Q is closed by A6; ::_thesis: ( Q c= P & p in Int Q )
(Int P) ` c= Q ` by A8;
then Q c= Int P by SUBSET_1:12;
hence Q c= P by A10, XBOOLE_1:1; ::_thesis: p in Int Q
W c= Q by A9, SUBSET_1:23;
then W c= Int Q by A5, TOPS_1:24;
hence p in Int Q by A7; ::_thesis: verum
end;
end;
end;
assume A11: 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 ) ; ::_thesis: T is regular
let p be Point of T; :: according to COMPTS_1:def_2 ::_thesis: for b1 being Element of bool the carrier of T holds
( b1 = {} or not b1 is closed or not p in b1 ` or ex b2, b3 being Element of bool the carrier of T st
( b2 is open & b3 is open & p in b2 & b1 c= b3 & b2 misses b3 ) )
let P be Subset of T; ::_thesis: ( P = {} or not P is closed or not p in P ` or ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 ) )
assume that
P <> {} and
A12: ( P is closed & p in P ` ) ; ::_thesis: ex b1, b2 being Element of bool the carrier of T st
( b1 is open & b2 is open & p in b1 & P c= b2 & b1 misses b2 )
p in Int (P `) by A12, TOPS_1:23;
then consider Q being Subset of T such that
A13: Q is closed and
A14: Q c= P ` and
A15: p in Int Q by A11;
reconsider W = Int Q as Subset of T ;
take W ; ::_thesis: ex b1 being Element of bool the carrier of T st
( W is open & b1 is open & p in W & P c= b1 & W misses b1 )
take V = Q ` ; ::_thesis: ( W is open & V is open & p in W & P c= V & W misses V )
thus W is open ; ::_thesis: ( V is open & p in W & P c= V & W misses V )
thus V is open by A13; ::_thesis: ( p in W & P c= V & W misses V )
thus p in W by A15; ::_thesis: ( P c= V & W misses V )
(P `) ` c= V by A14, SUBSET_1:12;
hence P c= V ; ::_thesis: W misses V
Q misses V by XBOOLE_1:79;
hence W misses V by TOPS_1:16, XBOOLE_1:63; ::_thesis: verum
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
let T be non empty TopSpace; ::_thesis: ( T is regular implies ( 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 ) ) )
assume A1: T is regular ; ::_thesis: ( 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 ) )
hereby ::_thesis: ( ( for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ) implies T is locally-compact )
assume A2: T is locally-compact ; ::_thesis: for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact )
let x be Point of T; ::_thesis: ex Y being Subset of T st
( x in Int Y & Y is compact )
ex Y being Subset of T st
( x in Int Y & Y c= [#] T & Y is compact ) by A2, WAYBEL_3:def_9;
hence ex Y being Subset of T st
( x in Int Y & Y is compact ) ; ::_thesis: verum
end;
assume A3: for x being Point of T ex Y being Subset of T st
( x in Int Y & Y is compact ) ; ::_thesis: T is locally-compact
let x be Point of T; :: according to WAYBEL_3:def_9 ::_thesis: for b1 being Element of bool the carrier of T holds
( not x in b1 or not b1 is open or ex b2 being Element of bool the carrier of T st
( x in Int b2 & b2 c= b1 & b2 is compact ) )
let X be Subset of T; ::_thesis: ( not x in X or not X is open or ex b1 being Element of bool the carrier of T st
( x in Int b1 & b1 c= X & b1 is compact ) )
assume ( x in X & X is open ) ; ::_thesis: ex b1 being Element of bool the carrier of T st
( x in Int b1 & b1 c= X & b1 is compact )
then A4: x in Int X by TOPS_1:23;
consider Y being Subset of T such that
A5: x in Int Y and
A6: Y is compact by A3;
x in (Int X) /\ (Int Y) by A5, A4, XBOOLE_0:def_4;
then x in Int (X /\ Y) by TOPS_1:17;
then consider Q being Subset of T such that
A7: Q is closed and
A8: Q c= X /\ Y and
A9: x in Int Q by A1, Th27;
take Q ; ::_thesis: ( x in Int Q & Q c= X & Q is compact )
thus x in Int Q by A9; ::_thesis: ( Q c= X & Q is compact )
X /\ Y c= X by XBOOLE_1:17;
hence Q c= X by A8, XBOOLE_1:1; ::_thesis: Q is compact
X /\ Y c= Y by XBOOLE_1:17;
hence Q is compact by A6, A7, A8, COMPTS_1:9, XBOOLE_1:1; ::_thesis: verum
end;