:: Weights of Continuous Lattices :: by Robert Milewski :: :: Received January 6, 2000 :: Copyright (c) 2000-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 ORDERS_2, SETFAM_1, SUBSET_1, WAYBEL_0, TARSKI, XXREAL_0, LATTICES, ORDINAL2, WAYBEL23, YELLOW_1, YELLOW_0, WAYBEL_8, CARD_1, ORDINAL1, STRUCT_0, XBOOLE_0, PRE_TOPC, RLVECT_3, RCOMP_1, WAYBEL_3, FINSET_1, EQREL_1, ZFMISC_1, FUNCT_1, RELAT_1, WAYBEL11, YELLOW_9, WAYBEL19, PRELAMB, CANTOR_1, PROB_1, DIRAF, LATTICE3, RELAT_2, CARD_FIL, REWRITE1, PARTFUN1, FINSEQ_3, FINSEQ_1, ORDINAL4, WAYBEL_9, WELLORD1, CAT_1, WAYBEL31; notations TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_1, DOMAIN_1, FINSEQ_2, FINSEQ_3, ORDINAL1, CARD_1, STRUCT_0, PRE_TOPC, TOPS_2, CANTOR_1, ORDERS_2, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_9, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL19, WAYBEL23; constructors DOMAIN_1, NAT_1, FINSEQ_3, TOPS_2, CANTOR_1, WAYBEL_1, WAYBEL_8, WAYBEL11, YELLOW_9, WAYBEL19, WAYBEL23, RELSET_1, WAYBEL_2; registrations XBOOLE_0, SUBSET_1, RELSET_1, FINSET_1, CARD_1, FINSEQ_1, STRUCT_0, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2, YELLOW_3, WAYBEL_3, WAYBEL_4, WAYBEL_8, WAYBEL14, YELLOW_9, YELLOW11, WAYBEL19, WAYBEL23, YELLOW15, WAYBEL25, WAYBEL30, ORDINAL1, PRE_TOPC; requirements NUMERALS, BOOLE, SUBSET; begin scheme :: WAYBEL31:sch 1 UparrowUnion{L1()->RelStr,P[set]}: for S be Subset-Family of L1() st S = { X where X is Subset of L1() : P[X] } holds uparrow union S = union { uparrow X where X is Subset of L1() : P[X] }; scheme :: WAYBEL31:sch 2 DownarrowUnion{L1()->RelStr,P[set]}: for S be Subset-Family of L1() st S = { X where X is Subset of L1() : P[X] } holds downarrow union S = union { downarrow X where X is Subset of L1() : P[X]}; registration let L1 be lower-bounded continuous sup-Semilattice; let B1 be with_bottom CLbasis of L1; cluster InclPoset Ids subrelstr B1 -> algebraic; end; definition :: DEFINITION 4.5 let L1 be continuous sup-Semilattice; func CLweight L1 -> Cardinal equals :: WAYBEL31:def 1 meet the set of all card B1 where B1 is with_bottom CLbasis of L1 ; end; theorem :: WAYBEL31:1 for L1 be continuous sup-Semilattice for B1 be with_bottom CLbasis of L1 holds CLweight L1 c= card B1; theorem :: WAYBEL31:2 for L1 be continuous sup-Semilattice ex B1 be with_bottom CLbasis of L1 st card B1 = CLweight L1; theorem :: WAYBEL31:3 :: Under 4.5. for L1 be algebraic lower-bounded LATTICE holds CLweight L1 = card the carrier of CompactSublatt L1; theorem :: WAYBEL31:4 for T be non empty TopSpace for L1 be continuous sup-Semilattice st InclPoset the topology of T = L1 for B1 be with_bottom CLbasis of L1 holds B1 is Basis of T; theorem :: WAYBEL31:5 for T be non empty TopSpace for L1 be continuous lower-bounded LATTICE st InclPoset the topology of T = L1 for B1 be Basis of T for B2 be Subset of L1 st B1 = B2 holds finsups B2 is with_bottom CLbasis of L1; theorem :: WAYBEL31:6 :: PROPOSITION 4.6 (i) for T be T_0 non empty TopSpace for L1 be continuous lower-bounded sup-Semilattice st InclPoset the topology of T = L1 holds T is infinite implies weight T = CLweight L1; theorem :: WAYBEL31:7 :: PROPOSITION 4.6 (ii) (a) for T be T_0 non empty TopSpace for L1 be continuous sup-Semilattice st InclPoset the topology of T = L1 holds card the carrier of T c= card the carrier of L1; theorem :: WAYBEL31:8 :: PROPOSITION 4.6 (ii) (b) for T be T_0 non empty TopSpace st T is finite holds weight T = card the carrier of T; theorem :: WAYBEL31:9 :: PROPOSITION 4.6 (ii) (c) for T be TopStruct for L1 be continuous lower-bounded LATTICE st InclPoset the topology of T = L1 & T is finite holds CLweight L1 = card the carrier of L1; theorem :: WAYBEL31:10 for L1 be continuous lower-bounded sup-Semilattice for T1 be Scott TopAugmentation of L1 for T2 be Lawson correct TopAugmentation of L1 for B2 be Basis of T2 holds { uparrow V where V is Subset of T2 : V in B2 } is Basis of T1; theorem :: WAYBEL31:11 for L1 be up-complete non empty Poset st L1 is finite for x be Element of L1 holds x in compactbelow x; theorem :: WAYBEL31:12 for L1 be finite LATTICE holds L1 is arithmetic; registration cluster finite -> arithmetic for LATTICE; end; registration cluster reflexive transitive antisymmetric with_suprema with_infima lower-bounded 1-element finite strict for RelStr; end; theorem :: WAYBEL31:13 for L1 be finite LATTICE for B1 be with_bottom CLbasis of L1 holds card B1 = CLweight L1 iff B1 = the carrier of CompactSublatt L1; definition let L1 be non empty reflexive RelStr; let A be Subset of L1; let a be Element of L1; func Way_Up(a,A) -> Subset of L1 equals :: WAYBEL31:def 2 wayabove a \ uparrow A; end; theorem :: WAYBEL31:14 for L1 be non empty reflexive RelStr for a be Element of L1 holds Way_Up(a,{}(L1)) = wayabove a; theorem :: WAYBEL31:15 for L1 be non empty Poset for A be Subset of L1 for a be Element of L1 st a in uparrow A holds Way_Up(a,A) = {}; theorem :: WAYBEL31:16 for L1 be non empty finite reflexive transitive RelStr holds Ids L1 is finite ; theorem :: WAYBEL31:17 for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite for B1 be with_bottom CLbasis of L1 holds B1 is infinite; theorem :: WAYBEL31:18 for L1 be complete non empty Poset for x be Element of L1 holds x is compact implies x = inf wayabove x; theorem :: WAYBEL31:19 for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite for B1 be with_bottom CLbasis of L1 holds card { Way_Up(a,A) where a is Element of L1, A is finite Subset of L1 : a in B1 & A c= B1 } c= card B1; theorem :: WAYBEL31:20 for T be Lawson complete TopLattice for X be finite Subset of T holds (uparrow X)` is open & (downarrow X)` is open; theorem :: WAYBEL31:21 for L1 be continuous lower-bounded sup-Semilattice for T be Lawson correct TopAugmentation of L1 holds for B1 be with_bottom CLbasis of L1 holds { Way_Up(a,A) where a is Element of L1, A is finite Subset of L1 : a in B1 & A c= B1 } is Basis of T; theorem :: WAYBEL31:22 for L1 be continuous lower-bounded sup-Semilattice for T be Scott TopAugmentation of L1 for b be Basis of T holds { wayabove inf u where u is Subset of T : u in b } is Basis of T; theorem :: WAYBEL31:23 for L1 be continuous lower-bounded sup-Semilattice for T be Scott TopAugmentation of L1 for B1 be Basis of T st B1 is infinite holds { inf u where u is Subset of T : u in B1 } is infinite; theorem :: WAYBEL31:24 :: THEOREM 4.7 (1)=(2) for L1 be continuous lower-bounded sup-Semilattice for T be Scott TopAugmentation of L1 holds CLweight L1 = weight T; theorem :: WAYBEL31:25 :: THEOREM 4.7 (1)=(3) for L1 be continuous lower-bounded sup-Semilattice for T be Lawson correct TopAugmentation of L1 holds CLweight L1 = weight T; theorem :: WAYBEL31:26 for L1,L2 be non empty RelStr st L1,L2 are_isomorphic holds card the carrier of L1 = card the carrier of L2; theorem :: WAYBEL31:27 :: THEOREM 4.7 (1)=(4) for L1 be continuous lower-bounded sup-Semilattice for B1 be with_bottom CLbasis of L1 st card B1 = CLweight L1 holds CLweight L1 = CLweight InclPoset Ids subrelstr B1; registration let L1 be continuous lower-bounded sup-Semilattice; cluster InclPoset sigma L1 -> with_suprema continuous; end; theorem :: WAYBEL31:28 :: THEOREM 4.7 (5) for L1 be continuous lower-bounded sup-Semilattice holds CLweight L1 c= CLweight InclPoset sigma L1; theorem :: WAYBEL31:29 :: THEOREM 4.7 (6) for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite holds CLweight L1 = CLweight InclPoset sigma L1;