Volume 12, 2000

University of Bialystok

Copyright (c) 2000 Association of Mizar Users

### The abstract of the Mizar article:

### Weights of Continuous Lattices

**by****Robert Milewski**- Received January 6, 2000
- MML identifier: WAYBEL31

- [ Mizar article, MML identifier index ]

environ vocabulary ORDERS_1, SETFAM_1, WAYBEL_0, TARSKI, LATTICES, ORDINAL2, WAYBEL23, YELLOW_1, YELLOW_0, WAYBEL_8, CARD_1, ORDINAL1, SUBSET_1, PRE_TOPC, CANTOR_1, WAYBEL_3, BOOLE, FINSET_1, TSP_1, FUNCT_1, RELAT_1, WAYBEL11, YELLOW_9, WAYBEL19, PRELAMB, DIRAF, PROB_1, COMPTS_1, QUANTAL1, LATTICE3, REALSET1, RELAT_2, FILTER_2, FINSEQ_1, MATRIX_2, BHSP_3, FINSEQ_4, WAYBEL_9, WELLORD1, CAT_1, WAYBEL31, RLVECT_3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, STRUCT_0, FINSET_1, RELSET_1, GROUP_1, RELAT_1, REALSET1, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_4, MATRIX_2, ORDINAL1, CARD_1, PRE_TOPC, TSP_1, TOPS_2, CANTOR_1, ORDERS_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_9, WAYBEL_0, WAYBEL_1, WAYBEL_3, WAYBEL_8, WAYBEL_9, WAYBEL11, WAYBEL19, WAYBEL23; constructors NAT_1, GROUP_1, FINSEQ_4, MATRIX_2, TSP_1, TOPS_2, CANTOR_1, URYSOHN1, ORDERS_3, YELLOW_9, WAYBEL_1, WAYBEL_8, WAYBEL11, WAYBEL19, WAYBEL23, MEMBERED; clusters STRUCT_0, RELSET_1, FINSET_1, FINSEQ_1, CARD_1, TSP_1, SUBSET_1, CANTOR_1, LATTICE3, YELLOW_0, YELLOW_1, YELLOW_2, YELLOW_3, YELLOW_9, YELLOW11, YELLOW13, YELLOW15, WAYBEL_0, WAYBEL_3, WAYBEL_4, WAYBEL_8, WAYBEL14, WAYBEL19, WAYBEL23, WAYBEL25, WAYBEL30, ZFMISC_1; requirements NUMERALS, BOOLE, SUBSET; begin scheme 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 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]}; definition 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 {Card B1 where B1 is with_bottom CLbasis of L1 : not contradiction}; end; theorem :: WAYBEL31:1 for T be TopStruct for b be Basis of T holds weight T c= Card b; theorem :: WAYBEL31:2 for T be TopStruct ex b be Basis of T st Card b = weight T; theorem :: WAYBEL31:3 for L1 be continuous sup-Semilattice for B1 be with_bottom CLbasis of L1 holds CLweight L1 c= Card B1; theorem :: WAYBEL31:4 for L1 be continuous sup-Semilattice ex B1 be with_bottom CLbasis of L1 st Card B1 = CLweight L1; theorem :: WAYBEL31:5 :: Under 4.5. for L1 be algebraic lower-bounded LATTICE holds CLweight L1 = Card the carrier of CompactSublatt L1; theorem :: WAYBEL31:6 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:7 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:8 :: 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:9 :: 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:10 :: 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:11 :: 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:12 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; canceled; theorem :: WAYBEL31:14 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:15 for L1 be finite LATTICE holds L1 is arithmetic; definition cluster finite -> arithmetic LATTICE; end; definition cluster trivial reflexive transitive antisymmetric with_suprema with_infima lower-bounded non empty finite strict RelStr; end; theorem :: WAYBEL31:16 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:17 for L1 be non empty reflexive RelStr for a be Element of L1 holds Way_Up(a,{}(L1)) = wayabove a; theorem :: WAYBEL31:18 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:19 for L1 be non empty finite reflexive transitive RelStr holds Ids L1 is finite; theorem :: WAYBEL31:20 for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite for B1 be with_bottom CLbasis of L1 holds B1 is infinite; canceled 2; theorem :: WAYBEL31:23 for L1 be complete (non empty Poset) for x be Element of L1 holds x is compact implies x = inf wayabove x; theorem :: WAYBEL31:24 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:25 for T be Lawson (complete TopLattice) for X be finite Subset of T holds (uparrow X)` is open & (downarrow X)` is open; theorem :: WAYBEL31:26 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:27 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:28 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:29 :: 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:30 :: 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:31 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:32 :: 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; definition let L1 be continuous lower-bounded sup-Semilattice; cluster InclPoset sigma L1 -> with_suprema continuous; end; theorem :: WAYBEL31:33 :: THEOREM 4.7 (5) for L1 be continuous lower-bounded sup-Semilattice holds CLweight L1 c= CLweight InclPoset sigma L1; theorem :: WAYBEL31:34 :: THEOREM 4.7 (6) for L1 be continuous lower-bounded sup-Semilattice st L1 is infinite holds CLweight L1 = CLweight InclPoset sigma L1;

Back to top