Volume 9, 1997

University of Bialystok

Copyright (c) 1997 Association of Mizar Users

### The abstract of the Mizar article:

### Baire Spaces, Sober Spaces

**by****Andrzej Trybulec**- Received January 8, 1997
- MML identifier: YELLOW_8

- [ Mizar article, MML identifier index ]

environ vocabulary FINSUB_1, FINSET_1, SETFAM_1, BOOLE, REALSET1, SUBSET_1, TARSKI, FUNCT_1, RELAT_1, CARD_4, CARD_1, CANTOR_1, PRE_TOPC, TOPS_1, TOPS_3, WAYBEL_6, YELLOW_6, TSP_1, SETWISEO, URYSOHN1, COMPTS_1, WAYBEL_3, YELLOW_8, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, CANTOR_1, SETFAM_1, WELLORD2, CARD_1, CARD_4, REALSET1, FINSET_1, FINSUB_1, SETWISEO, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_3, TSP_1, URYSOHN1, YELLOW_6, COMPTS_1, WAYBEL_3; constructors CANTOR_1, TOPS_1, CARD_4, TOPS_3, URYSOHN1, COMPTS_1, REALSET1, DOMAIN_1, T_0TOPSP, SETWISEO, WAYBEL_3, MEMBERED; clusters SUBSET_1, YELLOW_6, PRE_TOPC, CARD_5, FINSET_1, STRUCT_0, FINSUB_1, ARYTM_3, SETFAM_1, MEMBERED, ZFMISC_1; requirements NUMERALS, 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; definition let X be non empty set; redefine attr X is trivial means :: YELLOW_8:def 1 for x,y being Element of X holds x = y; end; begin :: Families of complements theorem :: YELLOW_8:3 for X being set, F being Subset-Family of X for P being Subset of X holds P` in COMPLEMENT F iff P in F; theorem :: YELLOW_8:4 for X being set, F being Subset-Family of X holds F,COMPLEMENT F are_equipotent; theorem :: YELLOW_8:5 for X,Y being set st X,Y are_equipotent & X is countable holds Y is countable; theorem :: YELLOW_8:6 for X being set, F being Subset-Family of X holds COMPLEMENT COMPLEMENT F = F; theorem :: YELLOW_8:7 for X being set, F being Subset-Family of X for P being Subset of X holds P` in COMPLEMENT F iff P in F; theorem :: YELLOW_8:8 for X being set, F,G being Subset-Family of X st COMPLEMENT F c= COMPLEMENT G holds F c= G; theorem :: YELLOW_8:9 for X being set, F,G being Subset-Family of X holds COMPLEMENT F c= G iff F c= COMPLEMENT G; theorem :: YELLOW_8:10 for X being set, F,G being Subset-Family of X st COMPLEMENT F = COMPLEMENT G holds F = G; definition let X be set; let F,G be Subset of bool X; redefine func F \/ G -> Subset-Family of X; end; theorem :: YELLOW_8:11 for X being set, F,G being Subset-Family of X holds COMPLEMENT(F \/ G) = COMPLEMENT F \/ COMPLEMENT G; theorem :: YELLOW_8:12 for X being set, F being Subset-Family of X st F = {X} holds COMPLEMENT F = {{}}; definition let X be set, F be empty Subset-Family of X; cluster COMPLEMENT F -> empty; end; theorem :: YELLOW_8:13 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:14 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:15 for X being 1-sorted, F being Subset-Family of X holds Intersect COMPLEMENT F = (union F)`; theorem :: YELLOW_8:16 for X being 1-sorted, F being Subset-Family of X holds union COMPLEMENT F = (Intersect F)`; begin :: Topological preliminaries theorem :: YELLOW_8:17 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:18 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:19 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:20 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; mode Basis of x -> Subset-Family of T means :: YELLOW_8:def 2 it c= the topology of T & x in Intersect it & for S being Subset of T st S is open & x in S ex V being Subset of T st V in it & V c= S; end; theorem :: YELLOW_8:21 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:22 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:23 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 3 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:24 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 4 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; definition let T be TopStruct; cluster irreducible -> non empty 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 5 p in S & S c= Cl{p}; end; theorem :: YELLOW_8:25 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:26 for T being non empty TopSpace, p being Point of T holds Cl{p} is irreducible; definition let T be non empty TopSpace; cluster irreducible Subset of T; end; definition let T be non empty TopSpace; attr T is sober means :: YELLOW_8:def 6 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:27 for T being non empty TopSpace, p being Point of T holds p is_dense_point_of Cl{p}; theorem :: YELLOW_8:28 for T being non empty TopSpace, p being Point of T holds p is_dense_point_of {p}; theorem :: YELLOW_8:29 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:30 for T being Hausdorff (non empty TopSpace), S being irreducible Subset of T holds S is trivial; definition let T be Hausdorff (non empty TopSpace); cluster irreducible -> trivial Subset of T; end; theorem :: YELLOW_8:31 for T being Hausdorff (non empty TopSpace) holds T is sober; definition cluster Hausdorff -> sober (non empty TopSpace); end; definition cluster sober (non empty TopSpace); end; theorem :: YELLOW_8:32 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:33 for T being sober (non empty TopSpace) holds T is T_0; definition cluster sober -> T_0 (non empty TopSpace); end; definition let X be set; func CofinTop X -> strict TopStruct means :: YELLOW_8:def 7 the carrier of it = X & COMPLEMENT the topology of it = {X} \/ Fin X; end; definition let X be non empty set; cluster CofinTop X -> non empty; end; definition let X be set; cluster CofinTop X -> TopSpace-like; end; theorem :: YELLOW_8:34 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:35 for T being non empty TopSpace st T is_T1 for p being Point of T holds Cl{p} = {p}; definition let X be non empty set; cluster CofinTop X -> being_T1; end; definition let X be infinite set; cluster CofinTop X -> non sober; end; definition cluster being_T1 non sober (non empty TopSpace); end; begin :: More on regular spaces theorem :: YELLOW_8:36 for T being non empty TopSpace holds T is_T3 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:37 for T being non empty TopSpace st T is_T3 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;

Back to top