:: Baire Spaces, Sober Spaces :: by Andrzej Trybulec :: :: Received January 8, 1997 :: Copyright (c) 1997-2021 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;