:: Components and Basis of Topological Spaces :: by Robert Milewski :: :: Received June 22, 1999 :: Copyright (c) 1999-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 NUMBERS, NAT_1, XBOOLE_0, FINSEQ_1, FUNCT_1, RELAT_1, TARSKI, SUBSET_1, MARGREL1, FINSET_1, FINSEQ_2, CARD_1, SETFAM_1, STRUCT_0, ZFMISC_1, FUNCOP_1, XBOOLEAN, EQREL_1, ORDERS_2, WAYBEL23, YELLOW_0, LATTICES, ORDINAL2, WAYBEL_0, WAYBEL_3, WAYBEL_8, RCOMP_1, PRE_TOPC, RLVECT_3, CANTOR_1, YELLOW15; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, SETFAM_1, DOMAIN_1, CARD_1, NUMBERS, FINSET_1, STRUCT_0, MARGREL1, RELAT_1, FUNCT_1, RELSET_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, EQREL_1, FUNCOP_1, CARD_3, PRE_TOPC, TOPS_2, CANTOR_1, ORDERS_2, YELLOW_0, WAYBEL_0, WAYBEL_3, WAYBEL_8, WAYBEL23; constructors XXREAL_0, FINSEQ_4, REALSET1, VALUAT_1, TOPS_2, CANTOR_1, WAYBEL_8, WAYBEL23, RELSET_1, NUMBERS; registrations SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, FINSEQ_1, MARGREL1, FINSEQ_2, STRUCT_0, TOPS_1, LATTICE3, WAYBEL_0, WAYBEL_3, WAYBEL23, ORDINAL1, PRE_TOPC, ZFMISC_1, CARD_1, RELAT_1, FINSEQ_3; requirements NUMERALS, REAL, SUBSET, BOOLE; begin :: Preliminaries scheme :: YELLOW15:sch 1 SeqLambda1C{ i() -> Nat, D() -> non empty set, C[object], F, G(object)->set } : ex p be FinSequence of D() st len p = i() & for i be Nat st i in Seg i( ) holds (C[i] implies p.i = F(i)) & (not C[i] implies p.i = G(i)) provided for i be Nat st i in Seg i() holds (C[i] implies F(i) in D()) & (not C[i] implies G(i) in D()); begin :: Components definition let X be set; let p be FinSequence of bool X; let q be FinSequence of BOOLEAN; func MergeSequence(p,q) -> FinSequence of bool X means :: YELLOW15:def 1 len it = len p & for i be Nat st i in dom p holds it.i = IFEQ(q.i,TRUE,p.i,X\p.i); end; ::$CT 3 theorem :: YELLOW15:4 for X be set for p be FinSequence of bool X for q be FinSequence of BOOLEAN holds dom MergeSequence(p,q) = dom p; theorem :: YELLOW15:5 for X be set for p be FinSequence of bool X for q be FinSequence of BOOLEAN for i be Nat st q.i = TRUE holds MergeSequence(p,q).i = p.i; theorem :: YELLOW15:6 for X be set for p be FinSequence of bool X for q be FinSequence of BOOLEAN for i be Nat st i in dom p & q.i = FALSE holds MergeSequence(p,q).i = X\p.i; theorem :: YELLOW15:7 for X be set for q be FinSequence of BOOLEAN holds len MergeSequence( <*>(bool X),q) = 0; theorem :: YELLOW15:8 for X be set for q be FinSequence of BOOLEAN holds MergeSequence( <*>(bool X),q) = <*>(bool X); theorem :: YELLOW15:9 for X be set for x be Subset of X for q be FinSequence of BOOLEAN holds len MergeSequence(<*x*>,q) = 1; theorem :: YELLOW15:10 for X be set for x be Subset of X for q be FinSequence of BOOLEAN holds (q.1 = TRUE implies MergeSequence(<*x*>,q).1 = x) & (q.1 = FALSE implies MergeSequence(<*x*>,q).1 = X\x); theorem :: YELLOW15:11 for X be set for x,y be Subset of X for q be FinSequence of BOOLEAN holds len MergeSequence(<*x,y*>,q) = 2; theorem :: YELLOW15:12 for X be set for x,y be Subset of X for q be FinSequence of BOOLEAN holds (q.1 = TRUE implies MergeSequence(<*x,y*>,q).1 = x) & (q.1 = FALSE implies MergeSequence(<*x,y*>,q).1 = X\x) & (q.2 = TRUE implies MergeSequence( <*x,y*>,q).2 = y) & (q.2 = FALSE implies MergeSequence(<*x,y*>,q).2 = X\y); theorem :: YELLOW15:13 for X be set for x,y,z be Subset of X for q be FinSequence of BOOLEAN holds len MergeSequence(<*x,y,z*>,q) = 3; theorem :: YELLOW15:14 for X be set for x,y,z be Subset of X for q be FinSequence of BOOLEAN holds (q.1 = TRUE implies MergeSequence(<*x,y,z*>,q).1 = x) & (q.1 = FALSE implies MergeSequence(<*x,y,z*>,q).1 = X\x) & (q.2 = TRUE implies MergeSequence (<*x,y,z*>,q).2 = y) & (q.2 = FALSE implies MergeSequence(<*x,y,z*>,q).2 = X\y) & (q.3 = TRUE implies MergeSequence(<*x,y,z*>,q).3 = z) & (q.3 = FALSE implies MergeSequence(<*x,y,z*>,q).3 = X\z); theorem :: YELLOW15:15 for X be set for p be FinSequence of bool X holds { Intersect ( rng MergeSequence(p,q)) where q is FinSequence of BOOLEAN : len q = len p } is Subset-Family of X; registration cluster -> boolean-valued for FinSequence of BOOLEAN; end; definition let X be set; let Y be finite Subset-Family of X; func Components(Y) -> Subset-Family of X means :: YELLOW15:def 2 ex p be FinSequence of bool X st len p = card Y & rng p = Y & it = { Intersect (rng MergeSequence(p,q) ) where q is FinSequence of BOOLEAN : len q = len p }; end; registration let X be set; let Y be finite Subset-Family of X; cluster Components(Y) -> finite; end; theorem :: YELLOW15:16 for X be set for Y be empty Subset-Family of X holds Components( Y) = {X}; theorem :: YELLOW15:17 for X be set for Y,Z be finite Subset-Family of X st Z c= Y holds Components(Y) is_finer_than Components(Z); theorem :: YELLOW15:18 for X be set for Y be finite Subset-Family of X holds union Components(Y) = X ; theorem :: YELLOW15:19 for X be set for Y be finite Subset-Family of X for A,B be set st A in Components(Y) & B in Components(Y) & A <> B holds A misses B; definition let X be set; let Y be finite Subset-Family of X; attr Y is in_general_position means :: YELLOW15:def 3 not {} in Components(Y); end; theorem :: YELLOW15:20 for X be set for Y,Z be finite Subset-Family of X st Z is in_general_position & Y c= Z holds Y is in_general_position; theorem :: YELLOW15:21 for X be non empty set for Y be empty Subset-Family of X holds Y is in_general_position; theorem :: YELLOW15:22 for X be non empty set for Y be finite Subset-Family of X st Y is in_general_position holds Components(Y) is a_partition of X; begin :: About basis of Topological Spaces theorem :: YELLOW15:23 for L be non empty RelStr holds [#]L is infs-closed sups-closed; theorem :: YELLOW15:24 for L be non empty RelStr holds [#]L is with_bottom with_top; registration let L be non empty RelStr; cluster [#]L -> infs-closed sups-closed with_bottom with_top; end; theorem :: YELLOW15:25 for L be continuous sup-Semilattice holds [#]L is CLbasis of L; theorem :: YELLOW15:26 for L be up-complete non empty Poset st L is finite holds the carrier of L = the carrier of CompactSublatt L; theorem :: YELLOW15:27 for L be lower-bounded sup-Semilattice for B be Subset of L st B is infinite holds card B = card finsups B; theorem :: YELLOW15:28 for T be T_0 non empty TopSpace holds card the carrier of T c= card the topology of T; theorem :: YELLOW15:29 for T be TopStruct for X be Subset of T st X is open for B be finite Subset-Family of T st B is Basis of T for Y be set st Y in Components(B) holds X misses Y or Y c= X; theorem :: YELLOW15:30 for T be T_0 TopSpace st T is infinite for B be Basis of T holds B is infinite; theorem :: YELLOW15:31 for T be non empty TopSpace st T is finite for B be Basis of T for x be Element of T holds meet { A where A is Element of the topology of T : x in A } in B;