:: 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;