:: Baire Spaces, Sober Spaces
:: by Andrzej Trybulec
::
:: Received January 8, 1997
:: Copyright (c) 1997-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FINSUB_1, TARSKI, SETFAM_1, XBOOLE_0, ZFMISC_1, SUBSET_1,
FUNCT_1, RELAT_1, CARD_3, CARD_1, ORDINAL1, STRUCT_0, PRE_TOPC, RCOMP_1,
RLVECT_3, CANTOR_1, TOPS_1, TOPS_3, COMPTS_1, SETWISEO, FINSET_1, CARD_5,
WAYBEL_3, YELLOW_8;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, CANTOR_1,
SETFAM_1, ORDINAL1, CARD_1, CARD_3, FINSET_1, FINSUB_1, SETWISEO,
DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TOPS_3, COMPTS_1, WAYBEL_3;
constructors SETFAM_1, SETWISEO, REALSET1, TOPS_1, COMPTS_1, URYSOHN1, TOPS_3,
T_0TOPSP, CANTOR_1, WAYBEL_3, TOPS_2;
registrations XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, FINSUB_1, CARD_5,
STRUCT_0, PRE_TOPC, TOPS_1, PCOMPS_1;
requirements BOOLE, SUBSET;
definitions TARSKI, CANTOR_1, PRE_TOPC, WELLORD2, FUNCT_1, CARD_3, WAYBEL_3,
COMPTS_1, XBOOLE_0;
equalities STRUCT_0, SUBSET_1;
expansions TARSKI, PRE_TOPC, WAYBEL_3, XBOOLE_0;
theorems TOPS_1, PRE_TOPC, PCOMPS_1, CANTOR_1, TARSKI, ZFMISC_1, TOPS_3,
COMPTS_1, URYSOHN1, TSP_1, FINSUB_1, SETFAM_1, SUBSET_1, FUNCT_1, CARD_1,
XBOOLE_0, XBOOLE_1, TOPS_2;
schemes DOMAIN_1, FUNCT_1;
begin :: Preliminaries
theorem Th1:
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 such that
A1: A in Fin X and
A2: B c= A;
A c= X by A1,FINSUB_1:def 5;
then B c= X by A2;
hence thesis by A1,A2,FINSUB_1:def 5;
end;
theorem Th2:
for X being set, F being Subset-Family of X st F c= Fin X holds
meet F in Fin X
proof
let X be set, F be Subset-Family of X such that
A1: F c= Fin X;
per cases;
suppose
F = {};
hence thesis by FINSUB_1:7,SETFAM_1:1;
end;
suppose
F <> {};
then consider A being object such that
A2: A in F by XBOOLE_0:def 1;
reconsider A as set by TARSKI:1;
meet F c= A by A2,SETFAM_1:3;
hence thesis by A1,A2,Th1;
end;
end;
begin :: Families of complements
theorem Th3:
for X being set, F being Subset-Family of X holds F,COMPLEMENT F
are_equipotent
proof
let X be set, F be Subset-Family of X;
deffunc F(set) = 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 = F(x) from FUNCT_1:sch 5;
take f;
thus f is one-to-one
proof
let x1,x2 be object such that
A3: x1 in dom f and
A4: x2 in dom f and
A5: f.x1 = f.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;
end;
thus dom f = F by A1;
thus rng f c= COMPLEMENT F
proof
let e be object;
assume e in rng f;
then consider u being object 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 thesis by A1,A6,SETFAM_1:35;
end;
let e be object;
assume
A8: e in COMPLEMENT 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 thesis by A1,A9,FUNCT_1:def 3;
end;
theorem Th4:
for X,Y being set st X,Y are_equipotent & X is countable holds Y is countable
proof
let X,Y be set;
assume X,Y are_equipotent & card X c= omega;
hence card Y c= omega by CARD_1:5;
end;
theorem
for X being 1-sorted, F being Subset-Family of X, P being Subset of X
holds P` in COMPLEMENT F iff P in F
proof
let X be 1-sorted, F be Subset-Family of X, P be Subset of X;
P = (P`)`;
hence thesis by SETFAM_1:def 7;
end;
theorem Th6:
for X being 1-sorted, F being Subset-Family of X holds Intersect
COMPLEMENT F = (union F)`
proof
let X be 1-sorted, F be Subset-Family of X;
per cases;
suppose
A1: 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)`;
end;
suppose
F = {};
then reconsider G = F as empty Subset-Family of X;
COMPLEMENT G = {};
hence thesis by SETFAM_1:def 9,ZFMISC_1:2;
end;
end;
theorem Th7:
for X being 1-sorted, F being Subset-Family of X holds union
COMPLEMENT F = (Intersect F)`
proof
let X be 1-sorted, F be Subset-Family of X;
thus union COMPLEMENT F = (union COMPLEMENT F)``
.= (Intersect COMPLEMENT COMPLEMENT F)` by Th6
.= (Intersect F)`;
end;
begin :: Topological preliminaries
theorem
for T being non empty TopSpace, 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:
for T being TopStruct, B being Basis of T, 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, B be Basis of T, V be Subset of T such that
A1: V is open;
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 object holds x in V iff ex Y being set st x in Y & Y in X
proof
let x be object;
hereby
V in the topology of T by A1;
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;
then consider W being set such that
A5: x in W and
A6: W in Y by A4,TARSKI:def 4;
take W;
thus x in W by A5;
reconsider G = W as Subset of T by A6;
G c= V by A4,A6,ZFMISC_1:74;
hence W in X by A3,A6;
end;
given Y being set such that
A7: x in Y and
A8: Y in X;
ex G being Subset of T st Y = G & G in B & G c= V by A8;
hence thesis by A7;
end;
hence thesis by TARSKI:def 4;
end;
theorem Th10:
for T being TopStruct, B being Basis of T, S being Subset of T
st S in B holds S is open
proof
let T be TopStruct, B be Basis of T, S be Subset of T such that
A1: S in B;
B c= the topology of T by TOPS_2:64;
hence thesis by A1;
end;
theorem
for T being non empty TopSpace, B being Basis of T, 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, B be Basis of T, V be Subset of T;
set X = { G where G is Subset of T: G in B & G c= V }, Y = { G where G is
Subset of T: G in B & G c= Int V };
X = Y
proof
thus X c= Y
proof
let e be object;
assume e in X;
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 thesis by A1,A2;
end;
let e be object;
assume e in Y;
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;
hence thesis by A4;
end;
hence thesis by Th9;
end;
begin :: Baire Spaces
definition
let T be non empty TopStruct, x be Point of T, F be Subset-Family of T;
attr F is x-quasi_basis means
:Def1:
x in Intersect F &
for S being Subset of T st S is open & x in S ex V being Subset of T st
V in F & V c= S;
end;
registration
let T be non empty TopStruct, x be Point of T;
cluster open x-quasi_basis for Subset-Family of T;
existence
proof
defpred P[set] means $1 in the topology of T & x in $1;
set IT = { S where S is Subset of T: P[S]};
IT is Subset-Family of T from DOMAIN_1:sch 7;
then reconsider IT as Subset-Family of T;
take IT;
IT c= the topology of T
proof
let e be object;
assume e in IT;
then
ex S being Subset of T st S = e & S in the topology of T & x in S;
hence thesis;
end;
hence IT is open by TOPS_2:64;
now
let e be set;
assume e in IT;
then ex S being Subset of T st S = e & S in the topology of T & x in S;
hence x in e;
end;
hence x in Intersect IT by SETFAM_1:43;
let S be Subset of T such that
A1: S is open and
A2: x in S;
take V = S;
V in the topology of T by A1;
hence V in IT by A2;
thus thesis;
end;
end;
definition
let T be non empty TopStruct, x be Point of T;
mode Basis of x is open x-quasi_basis Subset-Family of T;
end;
theorem Th12:
for T being non empty TopStruct, x being Point of T, B being
Basis of x, V being Subset of T st V in B holds V is open & x in V
proof
let T be non empty TopStruct, x be Point of T, B be Basis of x, V be Subset
of T such that
A1: V in B;
B c= the topology of T by TOPS_2:64;
hence V is open by A1;
x in Intersect B by Def1;
hence thesis by A1,SETFAM_1:43;
end;
theorem
for T being non empty TopStruct, x being Point of T, B being Basis of
x, V being Subset of T st x in V & V is open ex W being Subset of T st W in B &
W c= V by Def1;
theorem
for T being non empty TopStruct, 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;
let P be Subset-Family of T such 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;
P is quasi_basis
proof
let e be object;
assume
A3: e in the topology of T;
then reconsider S = e as Subset of T;
set X = { V where V is Subset of T: V in P & V c= S };
A4: X c= P
proof
let e be object;
assume e in X;
then ex V being Subset of T st e = V & V in P & V c= S;
hence thesis;
end;
then reconsider X as Subset-Family of T by XBOOLE_1:1;
for u being object holds u in S iff ex Z being set st u in Z & Z in X
proof
let u be object;
hereby
assume
A5: u in S;
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;
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;
thus u in Z by A7,Th12;
thus Z in X by A6,A7,A8;
end;
given Z being set such that
A9: u in Z and
A10: Z in X;
ex V being Subset of T st V = Z & V in P & V c= S by A10;
hence thesis by A9;
end;
then S = union X by TARSKI:def 4;
hence thesis by A4,CANTOR_1:def 1;
end;
hence thesis by A1,TOPS_2:64;
end;
definition
let T be non empty TopSpace;
attr T is Baire means
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 ex I
being Subset of T st I = Intersect F & I is dense;
end;
theorem
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;
hereby
assume
A1: T is Baire;
let F be Subset-Family of T such that
A2: F is countable and
A3: for S being Subset of T st S in F holds S is nowhere_dense;
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;
assume S in G;
then S` in F by SETFAM_1:def 7;
then S` is nowhere_dense by A3;
hence thesis by TOPS_3:39;
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;
then (union F)` is dense by Th6;
hence union F is boundary by TOPS_1:def 4;
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;
let F be Subset-Family of T such that
A6: F is countable and
A7: for S being Subset of T st S in F holds S is everywhere_dense;
reconsider I = Intersect F as Subset of T;
take I;
thus I = Intersect F;
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;
assume S in G;
then S` in F by SETFAM_1:def 7;
then S` is everywhere_dense by A7;
hence thesis by TOPS_3:40;
end;
G is countable by A6,Th3,Th4;
then union G is boundary by A5,A8;
then (Intersect F)` is boundary by Th7;
hence thesis by TOPS_3:18;
end;
begin :: Sober Spaces
definition
let T be TopStruct, S be Subset of T;
attr S is irreducible means
:Def3:
S is non empty closed & for S1,S2 being
Subset of T st S1 is closed & S2 is closed & S = S1 \/ S2 holds S1 = S or S2 =
S;
end;
registration
let T be TopStruct;
cluster irreducible -> non empty for Subset of T;
coherence;
end;
definition
let T be non empty TopSpace, S be Subset of T;
let p be Point of T;
pred p is_dense_point_of S means
p in S & S c= Cl{p};
end;
theorem
for T being non empty TopSpace, S being Subset of T st S is closed 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:
for T being non empty TopSpace, p being Point of T holds Cl{p} is irreducible
proof
let T be non empty TopSpace, p be Point of T;
assume
A1: not thesis;
Cl{p} is non 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;
{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;
end;
registration
let T be non empty TopSpace;
cluster irreducible for Subset of T;
existence
proof
set p = the Point of T;
Cl{p} is irreducible by Th17;
hence thesis;
end;
end;
definition
let T be non empty TopSpace;
attr T is sober means
:Def5:
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;
theorem Th18:
for T being non empty TopSpace, p being Point of T holds p
is_dense_point_of Cl{p}
proof
let T be non empty TopSpace, p be Point of T;
{p} c= Cl{p} & p in {p} by PRE_TOPC:18,TARSKI:def 1;
hence p in Cl{p};
thus thesis;
end;
theorem Th19:
for T being non empty TopSpace, p being Point of T holds p
is_dense_point_of {p}
by TARSKI:def 1,PRE_TOPC:18;
theorem Th20:
for T being non empty TopSpace, 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, G,F be Subset of T such that
A1: G is open & F is closed;
F \ G = F /\ G` by SUBSET_1:13;
hence thesis by A1;
end;
theorem Th21:
for T being Hausdorff non empty TopSpace, S being irreducible
Subset of T holds S is trivial
proof
let T be Hausdorff non empty TopSpace, S be irreducible Subset of T;
assume S is non trivial;
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, S2 = S \ V;
A6: S1 <> S & S2 <> S by A4,A1,XBOOLE_0:def 5;
S is closed by Def3;
then
A7: S1 is closed & S2 is closed by A3,Th20;
A8: W /\ V = {} by A5;
S1 \/ S2 = S \ W /\ V by XBOOLE_1:54
.= S by A8;
hence contradiction by A7,A6,Def3;
end;
registration
let T be Hausdorff non empty TopSpace;
cluster irreducible -> trivial for Subset of T;
coherence by Th21;
end;
theorem Th22:
for T being Hausdorff non empty TopSpace holds T is sober
proof
let T be Hausdorff non empty TopSpace;
let S be irreducible Subset of T;
consider d be Element of S such that
A1: S = {d} by SUBSET_1:46;
reconsider d as Point of T;
take d;
thus d is_dense_point_of S by A1,Th19;
let p be Point of T;
assume p is_dense_point_of S;
then p in S;
hence thesis by A1,TARSKI:def 1;
end;
registration
cluster Hausdorff -> sober for non empty TopSpace;
coherence by Th22;
end;
registration
cluster sober for non empty TopSpace;
existence
proof
set T = the Hausdorff non empty TopSpace;
take T;
thus thesis;
end;
end;
theorem Th23:
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;
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;
assume for p,q being Point of T st Cl{p} = Cl{q} holds p = q;
then for p,q being Point of T st p <> q holds Cl{p} <> Cl{q};
hence thesis by TSP_1:def 5;
end;
theorem Th24:
for T being sober non empty TopSpace holds T is T_0
proof
let T be sober non empty TopSpace;
for p,q being Point of T st Cl{p} = Cl{q} holds p = q
proof
let p,q be Point of T such that
A1: Cl{p} = Cl{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 thesis by A1,A2,Th18;
end;
hence thesis by Th23;
end;
registration
cluster sober -> T_0 for non empty TopSpace;
coherence by Th24;
end;
definition
let X be set;
func CofinTop X -> strict TopStruct means
:Def6:
the carrier of it = X & COMPLEMENT the topology of it = {X} \/ Fin X;
existence
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 as Subset-Family of X;
take T = TopStruct(#X,COMPLEMENT F#);
thus the carrier of T = X;
thus thesis;
end;
uniqueness by SETFAM_1:38;
end;
registration
let X be non empty set;
cluster CofinTop X -> non empty;
coherence by Def6;
end;
registration
let X be set;
cluster CofinTop X -> TopSpace-like;
coherence
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 as Subset-Family of X;
reconsider F as Subset-Family of X;
A1: the carrier of IT = X by Def6;
A2: COMPLEMENT the topology of IT = {X} \/ Fin X by Def6;
A3: the topology of IT = COMPLEMENT COMPLEMENT the topology of IT
.= 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 IT in the topology of IT by A1,A3,XBOOLE_0:def 3;
A4: {} in {{}} by TARSKI:def 1;
thus for a being Subset-Family of IT st a c= the topology of IT holds
union a in the topology of IT
proof
let a be Subset-Family of IT such that
A5: a c= the topology of IT;
set b = a /\ COMPLEMENT F;
reconsider b as Subset-Family of X;
reconsider 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,25;
A7: union a = union(a /\ the topology of IT) 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;
per cases;
suppose
b = {};
hence thesis by A3,A4,A7,XBOOLE_0:def 3,ZFMISC_1:2;
end;
suppose
A8: b <> {};
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 thesis by A3,A7,XBOOLE_0:def 3;
end;
end;
let a,b be Subset of IT such that
A10: a in the topology of IT and
A11: b in the topology of IT;
reconsider a9=a, b9=b as Subset of X by Def6;
per cases;
suppose
a = {} or b = {};
hence a /\ b in the topology of IT by A3,A4,XBOOLE_0:def 3;
end;
suppose
A12: a <> {} & b <> {};
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 IT by A3,XBOOLE_0:def 3;
end;
end;
end;
theorem Th25:
for X being non empty set, P being Subset of CofinTop X holds P
is closed iff P = X or P is finite
proof
let X be non empty set, P be Subset of CofinTop X;
set T = CofinTop X;
hereby
assume that
A1: P is closed and
A2: P <> X;
P` in the topology of T by A1,PRE_TOPC:def 2;
then P in COMPLEMENT the topology of T 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;
end;
assume
A4: P = X or P is finite;
the carrier of T = 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 T by Def6;
then P` in the topology of T by SETFAM_1:def 7;
then P` is open;
hence thesis;
end;
theorem Th26:
for T being non empty TopSpace st T is T_1 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 -> T_1;
coherence
proof
for p being Point of CofinTop X holds {p} is closed by Th25;
hence thesis by URYSOHN1:19;
end;
end;
registration
let X be infinite set;
cluster CofinTop X -> non sober;
coherence
proof
set T = CofinTop X;
reconsider S = [#]X as Subset of T by Def6;
S is irreducible
proof
X = [#]T by Def6;
hence S is non empty closed;
let S1,S2 be Subset of T such that
A1: S1 is closed & S2 is closed and
A2: S = S1 \/ S2;
assume S1 <> S & S2 <> S;
then reconsider S19=S1, S29=S2 as finite set by A1,Th25;
S = S19 \/ S29 by A2;
hence contradiction;
end;
then reconsider S as irreducible Subset of T;
take S;
let p be Point of T;
now
assume p is_dense_point_of S;
then S c= Cl{p};
then Cl{p} is infinite;
hence contradiction by Th26;
end;
hence thesis;
end;
end;
registration
cluster T_1 non sober for non empty TopSpace;
existence
proof
set X = the infinite set;
take CofinTop X;
thus thesis;
end;
end;
begin :: More on regular spaces
theorem Th27:
for T being non empty TopSpace holds T is regular iff for p
being Point of T, P being Subset of T st p in Int P ex Q being Subset of T st Q
is closed & Q c= P & p in Int Q
proof
let T be non empty TopSpace;
hereby
assume
A1: T is regular;
let p be Point of T, P be Subset of T;
assume p in Int P;
then
A2: p in (Int P)``;
per cases;
suppose
A3: P = [#]T;
take Q = [#]T;
thus Q is closed;
thus Q c= P by A3;
Int Q = Q by TOPS_1:15;
hence p in Int Q;
end;
suppose
P <> [#]T;
consider W,V being Subset of T such that
A4: W is open and
A5: V is open and
A6: p in W and
A7: (Int P)` c= V and
A8: W misses V by A1,A2;
A9: Int P c= P by TOPS_1:16;
take Q = V`;
thus Q is closed by A5;
(Int P)` c= Q` by A7;
then Q c= Int P by SUBSET_1:12;
hence Q c= P by A9;
W c= Q by A8,SUBSET_1:23;
then W c= Int Q by A4,TOPS_1:24;
hence p in Int Q by A6;
end;
end;
assume
A10: for p being Point of T, P being Subset of T st p in Int P ex Q
being Subset of T st Q is closed & Q c= P & p in Int Q;
let p be Point of T, P be Subset of T such that
P <> {} and
A11: P is closed & p in P`;
p in Int P` by A11,TOPS_1:23;
then consider Q being Subset of T such that
A12: Q is closed and
A13: Q c= P` and
A14: p in Int Q by A10;
reconsider W = Int Q as Subset of T;
take W, V = Q`;
thus W is open;
thus V is open by A12;
thus p in W by A14;
P`` c= V by A13,SUBSET_1:12;
hence P c= V;
Q misses V by XBOOLE_1:79;
hence thesis by TOPS_1:16,XBOOLE_1:63;
end;
theorem
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 such that
A1: T is regular;
hereby
assume
A2: T is locally-compact;
let x be Point of T;
ex Y being Subset of T st x in Int Y & Y c= [#]T & Y is compact by A2;
hence ex Y being Subset of T st x in Int Y & Y is compact;
end;
assume
A3: 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, X be Subset of T;
assume x in X & X is open;
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;
thus x in Int Q by A9;
X /\ Y c= X by XBOOLE_1:17;
hence Q c= X by A8;
X /\ Y c= Y by XBOOLE_1:17;
hence thesis by A6,A7,A8,COMPTS_1:9,XBOOLE_1:1;
end;