:: by Robert Milewski

::

:: Received January 6, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

registration

let L1 be lower-bounded continuous sup-Semilattice;

let B1 be with_bottom CLbasis of L1;

coherence

InclPoset (Ids (subrelstr B1)) is algebraic by WAYBEL13:10;

end;
let B1 be with_bottom CLbasis of L1;

coherence

InclPoset (Ids (subrelstr B1)) is algebraic by WAYBEL13:10;

definition

let L1 be continuous sup-Semilattice;

meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } is Cardinal

end;
func CLweight L1 -> Cardinal equals :: WAYBEL31:def 1

meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;

coherence meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;

meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } is Cardinal

proof end;

:: deftheorem defines CLweight WAYBEL31:def 1 :

for L1 being continuous sup-Semilattice holds CLweight L1 = meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;

for L1 being continuous sup-Semilattice holds CLweight L1 = meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;

theorem Th1: :: WAYBEL31:1

for L1 being continuous sup-Semilattice

for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1

for B1 being with_bottom CLbasis of L1 holds CLweight L1 c= card B1

proof end;

theorem Th2: :: WAYBEL31:2

for L1 being continuous sup-Semilattice ex B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1

proof end;

theorem Th3: :: WAYBEL31:3

for L1 being lower-bounded algebraic LATTICE holds CLweight L1 = card the carrier of (CompactSublatt L1)

proof end;

theorem Th4: :: WAYBEL31:4

for T being non empty TopSpace

for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds

for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T

for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds

for B1 being with_bottom CLbasis of L1 holds B1 is Basis of T

proof end;

theorem Th5: :: WAYBEL31:5

for T being non empty TopSpace

for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds

for B1 being Basis of T

for B2 being Subset of L1 st B1 = B2 holds

finsups B2 is with_bottom CLbasis of L1

for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 holds

for B1 being Basis of T

for B2 being Subset of L1 st B1 = B2 holds

finsups B2 is with_bottom CLbasis of L1

proof end;

theorem Th6: :: WAYBEL31:6

for T being non empty T_0 TopSpace

for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & T is infinite holds

weight T = CLweight L1

for L1 being lower-bounded continuous sup-Semilattice st InclPoset the topology of T = L1 & T is infinite holds

weight T = CLweight L1

proof end;

theorem Th7: :: WAYBEL31:7

for T being non empty T_0 TopSpace

for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds

card the carrier of T c= card the carrier of L1

for L1 being continuous sup-Semilattice st InclPoset the topology of T = L1 holds

card the carrier of T c= card the carrier of L1

proof end;

theorem Th9: :: WAYBEL31:9

for T being TopStruct

for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds

CLweight L1 = card the carrier of L1

for L1 being lower-bounded continuous LATTICE st InclPoset the topology of T = L1 & T is finite holds

CLweight L1 = card the carrier of L1

proof end;

theorem Th10: :: WAYBEL31:10

for L1 being lower-bounded continuous sup-Semilattice

for T1 being Scott TopAugmentation of L1

for T2 being correct Lawson TopAugmentation of L1

for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1

for T1 being Scott TopAugmentation of L1

for T2 being correct Lawson TopAugmentation of L1

for B2 being Basis of T2 holds { (uparrow V) where V is Subset of T2 : V in B2 } is Basis of T1

proof end;

Lm1: for L1 being lower-bounded continuous sup-Semilattice

for T1 being Scott TopAugmentation of L1

for T2 being correct Lawson TopAugmentation of L1 holds weight T1 c= weight T2

proof end;

theorem Th11: :: WAYBEL31:11

for L1 being non empty up-complete Poset st L1 is finite holds

for x being Element of L1 holds x in compactbelow x

for x being Element of L1 holds x in compactbelow x

proof end;

registration

for b_{1} being LATTICE st b_{1} is finite holds

b_{1} is arithmetic
by Th12;

end;

cluster finite reflexive transitive antisymmetric with_suprema with_infima -> arithmetic for RelStr ;

coherence for b

b

registration

ex b_{1} being RelStr st

( b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is with_suprema & b_{1} is with_infima & b_{1} is lower-bounded & b_{1} is 1 -element & b_{1} is finite & b_{1} is strict )
end;

cluster finite 1 -element strict reflexive transitive antisymmetric lower-bounded with_suprema with_infima for RelStr ;

existence ex b

( b

proof end;

theorem Th13: :: WAYBEL31:13

for L1 being finite LATTICE

for B1 being with_bottom CLbasis of L1 holds

( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )

for B1 being with_bottom CLbasis of L1 holds

( card B1 = CLweight L1 iff B1 = the carrier of (CompactSublatt L1) )

proof end;

definition

let L1 be non empty reflexive RelStr ;

let A be Subset of L1;

let a be Element of L1;

coherence

(wayabove a) \ (uparrow A) is Subset of L1 ;

end;
let A be Subset of L1;

let a be Element of L1;

coherence

(wayabove a) \ (uparrow A) is Subset of L1 ;

:: deftheorem defines Way_Up WAYBEL31:def 2 :

for L1 being non empty reflexive RelStr

for A being Subset of L1

for a being Element of L1 holds Way_Up (a,A) = (wayabove a) \ (uparrow A);

for L1 being non empty reflexive RelStr

for A being Subset of L1

for a being Element of L1 holds Way_Up (a,A) = (wayabove a) \ (uparrow A);

theorem :: WAYBEL31:14

theorem :: WAYBEL31:15

for L1 being non empty Poset

for A being Subset of L1

for a being Element of L1 st a in uparrow A holds

Way_Up (a,A) = {}

for A being Subset of L1

for a being Element of L1 st a in uparrow A holds

Way_Up (a,A) = {}

proof end;

theorem Th17: :: WAYBEL31:17

for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds

for B1 being with_bottom CLbasis of L1 holds B1 is infinite

for B1 being with_bottom CLbasis of L1 holds B1 is infinite

proof end;

theorem :: WAYBEL31:18

for L1 being non empty complete Poset

for x being Element of L1 st x is compact holds

x = inf (wayabove x)

for x being Element of L1 st x is compact holds

x = inf (wayabove x)

proof end;

theorem Th19: :: WAYBEL31:19

for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds

for B1 being 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

for B1 being 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

proof end;

theorem Th20: :: WAYBEL31:20

for T being complete Lawson TopLattice

for X being finite Subset of T holds

( (uparrow X) ` is open & (downarrow X) ` is open )

for X being finite Subset of T holds

( (uparrow X) ` is open & (downarrow X) ` is open )

proof end;

theorem Th21: :: WAYBEL31:21

for L1 being lower-bounded continuous sup-Semilattice

for T being correct Lawson TopAugmentation of L1

for B1 being 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

for T being correct Lawson TopAugmentation of L1

for B1 being 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

proof end;

Lm2: for L1 being lower-bounded continuous sup-Semilattice

for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1

proof end;

theorem Th22: :: WAYBEL31:22

for L1 being lower-bounded continuous sup-Semilattice

for T being Scott TopAugmentation of L1

for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T

for T being Scott TopAugmentation of L1

for b being Basis of T holds { (wayabove (inf u)) where u is Subset of T : u in b } is Basis of T

proof end;

theorem Th23: :: WAYBEL31:23

for L1 being lower-bounded continuous sup-Semilattice

for T being Scott TopAugmentation of L1

for B1 being Basis of T st B1 is infinite holds

{ (inf u) where u is Subset of T : u in B1 } is infinite

for T being Scott TopAugmentation of L1

for B1 being Basis of T st B1 is infinite holds

{ (inf u) where u is Subset of T : u in B1 } is infinite

proof end;

Lm3: for L1 being lower-bounded continuous sup-Semilattice

for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T

proof end;

theorem Th24: :: WAYBEL31:24

for L1 being lower-bounded continuous sup-Semilattice

for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T

for T being Scott TopAugmentation of L1 holds CLweight L1 = weight T

proof end;

theorem :: WAYBEL31:25

for L1 being lower-bounded continuous sup-Semilattice

for T being correct Lawson TopAugmentation of L1 holds CLweight L1 = weight T

for T being correct Lawson TopAugmentation of L1 holds CLweight L1 = weight T

proof end;

theorem Th26: :: WAYBEL31:26

for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds

card the carrier of L1 = card the carrier of L2

card the carrier of L1 = card the carrier of L2

proof end;

theorem :: WAYBEL31:27

for L1 being lower-bounded continuous sup-Semilattice

for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds

CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))

for B1 being with_bottom CLbasis of L1 st card B1 = CLweight L1 holds

CLweight L1 = CLweight (InclPoset (Ids (subrelstr B1)))

proof end;

registration

let L1 be lower-bounded continuous sup-Semilattice;

coherence

( InclPoset (sigma L1) is with_suprema & InclPoset (sigma L1) is continuous )

end;
coherence

( InclPoset (sigma L1) is with_suprema & InclPoset (sigma L1) is continuous )

proof end;

theorem :: WAYBEL31:28

for L1 being lower-bounded continuous sup-Semilattice holds CLweight L1 c= CLweight (InclPoset (sigma L1))

proof end;

theorem :: WAYBEL31:29

for L1 being lower-bounded continuous sup-Semilattice st L1 is infinite holds

CLweight L1 = CLweight (InclPoset (sigma L1))

CLweight L1 = CLweight (InclPoset (sigma L1))

proof end;