:: On the characteristic and weight of a topological space :: by Grzegorz Bancerek :: :: Received December 10, 2004 :: Copyright (c) 2004-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 XBOOLE_0, PRE_TOPC, RLVECT_3, SUBSET_1, TARSKI, SETFAM_1, RCOMP_1, YELLOW_8, PBOOLE, FUNCT_1, CARD_3, ZFMISC_1, STRUCT_0, RELAT_1, CARD_1, ORDINAL1, FRECHET, WAYBEL23, FINSET_1, EQREL_1, NATTRA_1, CARD_2, CANTOR_1, TOPS_1, FINSUB_1, FINSEQ_1, PCOMPS_1, YELLOW_9, TOPGEN_2; notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, DOMAIN_1, SETFAM_1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, CARD_1, FINSEQ_1, CARD_3, EQREL_1, ORDINAL1, FINSET_1, FINSUB_1, CARD_2, STRUCT_0, PRE_TOPC, TOPS_1, TOPS_2, TDLAT_3, PCOMPS_1, CANTOR_1, FRECHET, YELLOW_8, YELLOW_9, WAYBEL23; constructors DOMAIN_1, FINSUB_1, CARD_2, TOPS_1, TOPS_2, TDLAT_3, CANTOR_1, YELLOW_8, YELLOW_9, FRECHET, WAYBEL23, RELSET_1, FINSEQ_2, XTUPLE_0; registrations SUBSET_1, FINSET_1, CARD_1, EQREL_1, CARD_5, CARD_FIL, STRUCT_0, PRE_TOPC, TOPS_1, TDLAT_3, YELLOW12, ORDINAL1, COMPTS_1, RELSET_1; requirements BOOLE, SUBSET, NUMERALS; begin :: The characteristic of a topological space reserve a,b,c for set; :: theorem :: TOPGEN_2:1 for T being non empty TopSpace, B being Basis of T for x being Element of T holds {U where U is Subset of T: x in U & U in B} is Basis of x; :: theorem :: TOPGEN_2:2 for T being non empty TopSpace for B being ManySortedSet of T st for x being Element of T holds B.x is Basis of x holds Union B is Basis of T; definition let T be non empty TopStruct; let x be Element of T; func Chi(x,T) -> cardinal number means :: TOPGEN_2:def 1 (ex B being Basis of x st it = card B) & for B being Basis of x holds it c= card B; end; :: theorem :: TOPGEN_2:3 for X being set st for a being set st a in X holds a is cardinal number holds union X is cardinal number; definition let T be non empty TopStruct; func Chi(T) -> cardinal number means :: TOPGEN_2:def 2 (for x being Point of T holds Chi(x,T) c= it) & for M being cardinal number st for x being Point of T holds Chi(x,T) c= M holds it c= M; end; :: theorem :: TOPGEN_2:4 for T being non empty TopStruct holds Chi(T) = union the set of all Chi(x,T) where x is Point of T; theorem :: TOPGEN_2:5 for T being non empty TopStruct for x being Point of T holds Chi( x,T) c= Chi(T); :: theorem :: TOPGEN_2:6 for T being non empty TopSpace holds T is first-countable iff Chi(T) c= omega ; begin :: Neighborhood system definition let T be non empty TopSpace; mode Neighborhood_System of T -> ManySortedSet of T means :: TOPGEN_2:def 3 for x being Element of T holds it.x is Basis of x; end; :: definition let T be non empty TopSpace; let N be Neighborhood_System of T; redefine func Union N -> Basis of T; let x be Point of T; redefine func N.x -> Basis of x; end; :: :: for T being non empty TopSpace :: for N being Neighborhood_System of T :: for x being Element of T holds N.x is non empty & :: for U being set st U in N.x holds x in U :: by YELLOW_8:21; :: and clusters YELLOW12 :: theorem :: TOPGEN_2:7 for T being non empty TopSpace for x,y being Point of T for B1 being Basis of x, B2 being Basis of y for U being set st x in U & U in B2 ex V being open Subset of T st V in B1 & V c= U; :: theorem :: TOPGEN_2:8 for T being non empty TopSpace for x being Point of T for B being Basis of x for U1,U2 being set st U1 in B & U2 in B ex V being open Subset of T st V in B & V c= U1 /\ U2; :: theorem :: TOPGEN_2:9 for T being non empty TopSpace for A being Subset of T for x being Element of T holds x in Cl A iff for B being Basis of x for U being set st U in B holds U meets A; :: theorem :: TOPGEN_2:10 for T being non empty TopSpace for A being Subset of T for x being Element of T holds x in Cl A iff ex B being Basis of x st for U being set st U in B holds U meets A; registration let T be TopSpace; cluster open non empty for Subset-Family of T; end; begin :: The weight of a topological space :: theorem :: TOPGEN_2:11 for T being non empty TopSpace for S being open Subset-Family of T ex G being open Subset-Family of T st G c= S & union G = union S & card G c= weight T; definition let T be TopStruct; attr T is finite-weight means :: TOPGEN_2:def 4 weight T is finite; end; notation let T be TopStruct; antonym T is infinite-weight for T is finite-weight; end; registration cluster finite -> finite-weight for TopStruct; cluster infinite-weight -> infinite for TopStruct; end; theorem :: TOPGEN_2:12 for X being set holds card SmallestPartition X = card X; theorem :: TOPGEN_2:13 for T being discrete non empty TopStruct holds SmallestPartition the carrier of T is Basis of T & for B being Basis of T holds SmallestPartition the carrier of T c= B; theorem :: TOPGEN_2:14 for T being discrete non empty TopStruct holds weight T = card the carrier of T; registration cluster infinite-weight for TopSpace; end; theorem :: TOPGEN_2:15 for T being finite-weight non empty TopSpace ex B0 being Basis of T st ex f being Function of the carrier of T, the topology of T st B0 = rng f & for x being Point of T holds x in f.x & for U being open Subset of T st x in U holds f.x c= U; theorem :: TOPGEN_2:16 for T being TopSpace for B0,B being Basis of T for f being Function of the carrier of T, the topology of T st B0 = rng f & for x being Point of T holds x in f.x & for U being open Subset of T st x in U holds f.x c= U holds B0 c= B; theorem :: TOPGEN_2:17 for T being TopSpace for B0 being Basis of T for f being Function of the carrier of T, the topology of T st B0 = rng f & for x being Point of T holds x in f.x & for U being open Subset of T st x in U holds f.x c= U holds weight T = card B0; :: theorem :: TOPGEN_2:18 for T being non empty TopSpace for B being Basis of T ex B1 being Basis of T st B1 c= B & card B1 = weight T; begin :: Example 1.1.8: Almost discrete topological space with infinity definition let X, x0 be set; func DiscrWithInfin(X,x0) -> strict TopStruct means :: TOPGEN_2:def 5 the carrier of it = X & the topology of it = {U where U is Subset of X: not x0 in U} \/ {F` where F is Subset of X: F is finite}; end; registration let X,x0 be set; cluster DiscrWithInfin(X,x0) -> TopSpace-like; end; registration let X be non empty set, x0 be set; cluster DiscrWithInfin(X,x0) -> non empty; end; theorem :: TOPGEN_2:19 for X,x0 being set, A being Subset of DiscrWithInfin(X,x0) holds A is open iff not x0 in A or A` is finite; theorem :: TOPGEN_2:20 for X,x0 being set, A being Subset of DiscrWithInfin(X,x0) holds A is closed iff (x0 in X implies x0 in A) or A is finite; theorem :: TOPGEN_2:21 for X,x0,x being set st x in X holds {x} is closed Subset of DiscrWithInfin(X,x0); theorem :: TOPGEN_2:22 for X,x0,x being set st x in X & x <> x0 holds {x} is open Subset of DiscrWithInfin(X,x0); theorem :: TOPGEN_2:23 for X,x0 being set st X is infinite for U being Subset of DiscrWithInfin(X,x0) st U = {x0} holds U is not open; theorem :: TOPGEN_2:24 for X,x0 being set for A being Subset of DiscrWithInfin(X,x0) st A is finite holds Cl A = A; theorem :: TOPGEN_2:25 for T being non empty TopSpace for A being Subset of T st A is not closed for a being Point of T st A \/ {a} is closed holds Cl A = A \/ {a} ; theorem :: TOPGEN_2:26 for X,x0 being set st x0 in X for A being Subset of DiscrWithInfin(X,x0) st A is infinite holds Cl A = A \/ {x0}; theorem :: TOPGEN_2:27 for X,x0 being set for A being Subset of DiscrWithInfin(X,x0) st A` is finite holds Int A = A; theorem :: TOPGEN_2:28 for X,x0 being set st x0 in X for A being Subset of DiscrWithInfin(X, x0) st A` is infinite holds Int A = A \ {x0}; theorem :: TOPGEN_2:29 for X, x0 being set holds ex B0 being Basis of DiscrWithInfin(X, x0) st B0 = ((SmallestPartition X) \ {{x0}}) \/ {F` where F is Subset of X: F is finite}; theorem :: TOPGEN_2:30 for X being infinite set holds card Fin X = card X; theorem :: TOPGEN_2:31 for X being infinite set holds card {F` where F is Subset of X: F is finite} = card X; theorem :: TOPGEN_2:32 for X being infinite set, x0 being set for B0 being Basis of DiscrWithInfin(X,x0) st B0 = ((SmallestPartition X) \ {{x0}}) \/ {F` where F is Subset of X: F is finite} holds card B0 = card X; theorem :: TOPGEN_2:33 for X being infinite set, x0 being set for B being Basis of DiscrWithInfin(X,x0) holds card X c= card B; theorem :: TOPGEN_2:34 for X being infinite set, x0 being set holds weight DiscrWithInfin(X, x0) = card X; theorem :: TOPGEN_2:35 for X being non empty set, x0 being set holds ex B0 being prebasis of DiscrWithInfin(X,x0) st B0 = ((SmallestPartition X) \ {{x0}}) \/ the set of all {x}` where x is Element of X; begin :: Exercises :: theorem :: TOPGEN_2:36 for T being TopSpace, F being Subset-Family of T for I being non empty Subset-Family of F st for G being set st G in I holds F\G is finite holds Cl union F = union clf F \/ meet {Cl union G where G is Subset-Family of T: G in I }; :: theorem :: TOPGEN_2:37 for T being TopSpace, F being Subset-Family of T holds Cl union F = union clf F \/ meet {Cl union G where G is Subset-Family of T: G c= F & F\G is finite}; :: theorem :: TOPGEN_2:38 for X being set, O being Subset-Family of bool X st for o being Subset-Family of X st o in O holds TopStruct(#X,o#) is TopSpace ex B being Subset-Family of X st B = Intersect O & TopStruct(#X,B#) is TopSpace & (for o being Subset-Family of X st o in O holds TopStruct(#X,o#) is TopExtension of TopStruct(#X,B#)) & for T being TopSpace st the carrier of T = X & for o being Subset-Family of X st o in O holds TopStruct(#X,o#) is TopExtension of T holds TopStruct(#X,B#) is TopExtension of T; :: theorem :: TOPGEN_2:39 for X being set, O being Subset-Family of bool X ex B being Subset-Family of X st B = UniCl FinMeetCl union O & TopStruct(#X,B#) is TopSpace & (for o being Subset-Family of X st o in O holds TopStruct(#X,B#) is TopExtension of TopStruct(#X,o#)) & for T being TopSpace st the carrier of T = X & for o being Subset-Family of X st o in O holds T is TopExtension of TopStruct(#X,o#) holds T is TopExtension of TopStruct(#X,B#);