:: Baire Spaces, Sober Spaces
:: by Andrzej Trybulec
::
:: Received January 8, 1997
:: Copyright (c) 1997-2016 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;
begin :: Preliminaries
theorem :: YELLOW_8:1
for X,A,B being set st A in Fin X & B c= A holds B in Fin X;
theorem :: YELLOW_8:2
for X being set, F being Subset-Family of X st F c= Fin X holds
meet F in Fin X;
begin :: Families of complements
theorem :: YELLOW_8:3
for X being set, F being Subset-Family of X holds F,COMPLEMENT F
are_equipotent;
theorem :: YELLOW_8:4
for X,Y being set st X,Y are_equipotent & X is countable holds Y is countable
;
theorem :: YELLOW_8:5
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;
theorem :: YELLOW_8:6
for X being 1-sorted, F being Subset-Family of X holds Intersect
COMPLEMENT F = (union F)`;
theorem :: YELLOW_8:7
for X being 1-sorted, F being Subset-Family of X holds union
COMPLEMENT F = (Intersect F)`;
begin :: Topological preliminaries
theorem :: YELLOW_8:8
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;
theorem :: YELLOW_8:9
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 };
theorem :: YELLOW_8:10
for T being TopStruct, B being Basis of T, S being Subset of T
st S in B holds S is open;
theorem :: YELLOW_8:11
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 };
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
:: YELLOW_8:def 1
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;
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 :: YELLOW_8:12
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;
theorem :: YELLOW_8:13
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;
theorem :: YELLOW_8:14
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;
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 ex I
being Subset of T st I = Intersect F & I is dense;
end;
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;
begin :: Sober Spaces
definition
let T be TopStruct, S be Subset of T;
attr S is irreducible means
:: YELLOW_8:def 3
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;
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
:: YELLOW_8:def 4
p in S & S c= Cl{p};
end;
theorem :: YELLOW_8:16
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};
theorem :: YELLOW_8:17
for T being non empty TopSpace, p being Point of T holds Cl{p} is irreducible
;
registration
let T be non empty TopSpace;
cluster irreducible for Subset of T;
end;
definition
let T be non empty TopSpace;
attr T is sober means
:: 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;
theorem :: YELLOW_8:18
for T being non empty TopSpace, p being Point of T holds p
is_dense_point_of Cl{p};
theorem :: YELLOW_8:19
for T being non empty TopSpace, p being Point of T holds p
is_dense_point_of {p};
theorem :: YELLOW_8:20
for T being non empty TopSpace, G,F being Subset of T st G is
open & F is closed holds F \ G is closed;
theorem :: YELLOW_8:21
for T being Hausdorff non empty TopSpace, S being irreducible
Subset of T holds S is trivial;
registration
let T be Hausdorff non empty TopSpace;
cluster irreducible -> trivial for Subset of T;
end;
theorem :: YELLOW_8:22
for T being Hausdorff non empty TopSpace holds T is sober;
registration
cluster Hausdorff -> sober for non empty TopSpace;
end;
registration
cluster sober for non empty TopSpace;
end;
theorem :: 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;
theorem :: YELLOW_8:24
for T being sober non empty TopSpace holds T is T_0;
registration
cluster sober -> T_0 for non empty TopSpace;
end;
definition
let X be set;
func CofinTop X -> strict TopStruct means
:: YELLOW_8:def 6
the carrier of it = X & COMPLEMENT the topology of it = {X} \/ Fin X;
end;
registration
let X be non empty set;
cluster CofinTop X -> non empty;
end;
registration
let X be set;
cluster CofinTop X -> TopSpace-like;
end;
theorem :: YELLOW_8:25
for X being non empty set, P being Subset of CofinTop X holds P
is closed iff P = X or P is finite;
theorem :: YELLOW_8:26
for T being non empty TopSpace st T is T_1 for p being Point of
T holds Cl{p} = {p};
registration
let X be non empty set;
cluster CofinTop X -> T_1;
end;
registration
let X be infinite set;
cluster CofinTop X -> non sober;
end;
registration
cluster T_1 non sober for non empty TopSpace;
end;
begin :: More on regular spaces
theorem :: YELLOW_8:27
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;
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;