:: Introduction to Lattice Theory
:: by Stanis{\l}aw \.Zukowski
::
:: Received April 14, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem defines "\/" LATTICES:def 1 :
:: deftheorem defines "/\" LATTICES:def 2 :
:: deftheorem Def3 defines [= LATTICES:def 3 :
Lm1:
for uu, nn being BinOp of bool {}
for x, y being Element of LattStr(# (bool {} ),uu,nn #) holds x = y
Lm2:
for n being BinOp of bool {}
for x, y being Element of \/-SemiLattStr(# (bool {} ),n #) holds x = y
Lm3:
for n being BinOp of bool {}
for x, y being Element of /\-SemiLattStr(# (bool {} ),n #) holds x = y
:: deftheorem Def4 defines join-commutative LATTICES:def 4 :
:: deftheorem Def5 defines join-associative LATTICES:def 5 :
:: deftheorem Def6 defines meet-commutative LATTICES:def 6 :
:: deftheorem Def7 defines meet-associative LATTICES:def 7 :
:: deftheorem Def8 defines meet-absorbing LATTICES:def 8 :
:: deftheorem Def9 defines join-absorbing LATTICES:def 9 :
:: deftheorem Def10 defines Lattice-like LATTICES:def 10 :
:: deftheorem Def11 defines distributive LATTICES:def 11 :
:: deftheorem Def12 defines modular LATTICES:def 12 :
:: deftheorem Def13 defines lower-bounded LATTICES:def 13 :
:: deftheorem Def14 defines upper-bounded LATTICES:def 14 :
Lm4:
for n, u being BinOp of bool {} holds LattStr(# (bool {} ),n,u #) is Lattice
Lm5:
for n, u being BinOp of bool {} holds LattStr(# (bool {} ),n,u #) is 0_Lattice
Lm6:
for n, u being BinOp of bool {} holds LattStr(# (bool {} ),n,u #) is 1_Lattice
:: deftheorem Def15 defines bounded LATTICES:def 15 :
:: deftheorem Def16 defines Bottom LATTICES:def 16 :
:: deftheorem Def17 defines Top LATTICES:def 17 :
:: deftheorem Def18 defines is_a_complement_of LATTICES:def 18 :
:: deftheorem Def19 defines complemented LATTICES:def 19 :
:: deftheorem Def20 defines Boolean LATTICES:def 20 :
theorem :: LATTICES:1
canceled;
theorem :: LATTICES:2
canceled;
theorem :: LATTICES:3
canceled;
theorem :: LATTICES:4
canceled;
theorem :: LATTICES:5
canceled;
theorem :: LATTICES:6
canceled;
theorem :: LATTICES:7
canceled;
theorem :: LATTICES:8
canceled;
theorem :: LATTICES:9
canceled;
theorem :: LATTICES:10
canceled;
theorem :: LATTICES:11
canceled;
theorem :: LATTICES:12
canceled;
theorem :: LATTICES:13
canceled;
theorem :: LATTICES:14
canceled;
theorem :: LATTICES:15
canceled;
theorem :: LATTICES:16
canceled;
theorem Th17: :: LATTICES:17
theorem :: LATTICES:18
theorem Th19: :: LATTICES:19
theorem :: LATTICES:20
canceled;
theorem Th21: :: LATTICES:21
theorem Th22: :: LATTICES:22
theorem Th23: :: LATTICES:23
theorem :: LATTICES:24
canceled;
theorem :: LATTICES:25
theorem Th26: :: LATTICES:26
theorem Th27: :: LATTICES:27
theorem :: LATTICES:28
canceled;
theorem :: LATTICES:29
theorem :: LATTICES:30
canceled;
theorem Th31: :: LATTICES:31
theorem Th32: :: LATTICES:32
theorem :: LATTICES:33
canceled;
theorem :: LATTICES:34
theorem :: LATTICES:35
canceled;
theorem :: LATTICES:36
canceled;
theorem :: LATTICES:37
canceled;
theorem :: LATTICES:38
canceled;
theorem Th39: :: LATTICES:39
theorem :: LATTICES:40
theorem Th41: :: LATTICES:41
theorem :: LATTICES:42
canceled;
theorem Th43: :: LATTICES:43
theorem :: LATTICES:44
theorem :: LATTICES:45
:: deftheorem Def21 defines ` LATTICES:def 21 :
theorem :: LATTICES:46
canceled;
theorem Th47: :: LATTICES:47
theorem Th48: :: LATTICES:48
theorem Th49: :: LATTICES:49
theorem Th50: :: LATTICES:50
theorem :: LATTICES:51
theorem Th52: :: LATTICES:52
theorem :: LATTICES:53