:: Weights of Continuous Lattices
:: by Robert Milewski
::
:: Received January 6, 2000
:: Copyright (c) 2000 Association of Mizar Users
:: deftheorem defines CLweight WAYBEL31:def 1 :
theorem :: WAYBEL31:1
canceled;
theorem :: WAYBEL31:2
canceled;
theorem Th3: :: WAYBEL31:3
theorem Th4: :: WAYBEL31:4
theorem Th5: :: WAYBEL31:5
theorem Th6: :: WAYBEL31:6
theorem Th7: :: WAYBEL31:7
theorem Th8: :: WAYBEL31:8
theorem Th9: :: WAYBEL31:9
theorem Th10: :: WAYBEL31:10
theorem Th11: :: WAYBEL31:11
theorem Th12: :: WAYBEL31:12
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
theorem :: WAYBEL31:13
canceled;
theorem Th14: :: WAYBEL31:14
theorem Th15: :: WAYBEL31:15
theorem Th16: :: WAYBEL31:16
:: deftheorem defines Way_Up WAYBEL31:def 2 :
theorem :: WAYBEL31:17
theorem :: WAYBEL31:18
theorem Th19: :: WAYBEL31:19
theorem Th20: :: WAYBEL31:20
theorem :: WAYBEL31:21
canceled;
theorem :: WAYBEL31:22
canceled;
theorem :: WAYBEL31:23
theorem Th24: :: WAYBEL31:24
theorem Th25: :: WAYBEL31:25
theorem Th26: :: WAYBEL31:26
Lm2:
for L1 being lower-bounded continuous sup-Semilattice
for T being correct Lawson TopAugmentation of L1 holds weight T c= CLweight L1
theorem Th27: :: WAYBEL31:27
theorem Th28: :: WAYBEL31:28
Lm3:
for L1 being lower-bounded continuous sup-Semilattice
for T being Scott TopAugmentation of L1 holds CLweight L1 c= weight T
theorem Th29: :: WAYBEL31:29
theorem :: WAYBEL31:30
theorem Th31: :: WAYBEL31:31
theorem :: WAYBEL31:32
theorem :: WAYBEL31:33
theorem :: WAYBEL31:34