begin
Lm1:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )
Lm2:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )
Lm3:
for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )
Lm4:
for L being finite Lattice ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a
Lm5:
for L being finite Lattice holds L is complete
:: deftheorem defines % LATTICE6:def 1 :
:: deftheorem defines % LATTICE6:def 2 :
Lm6:
for L being finite Lattice holds (LattPOSet L) ~ is well_founded
:: deftheorem Def3 defines noetherian LATTICE6:def 3 :
:: deftheorem Def4 defines co-noetherian LATTICE6:def 4 :
theorem
Lm7:
for L being finite Lattice holds
( L is noetherian & L is co-noetherian )
:: deftheorem Def5 defines is-upper-neighbour-of LATTICE6:def 5 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem defines *' LATTICE6:def 6 :
:: deftheorem defines *' LATTICE6:def 7 :
:: deftheorem Def8 defines completely-meet-irreducible LATTICE6:def 8 :
:: deftheorem Def9 defines completely-join-irreducible LATTICE6:def 9 :
theorem Th9:
theorem
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
Lm8:
for L being Lattice
for a, b being Element of L holds
( a "/\" b = (a % ) "/\" (b % ) & a "\/" b = (a % ) "\/" (b % ) )
theorem Th17:
theorem Th18:
theorem Th19:
theorem
:: deftheorem Def10 defines atomic LATTICE6:def 10 :
:: deftheorem Def11 defines co-atomic LATTICE6:def 11 :
theorem
theorem
:: deftheorem Def12 defines atomic LATTICE6:def 12 :
Lm9:
ex L being Lattice st
( L is atomic & L is complete )
:: deftheorem Def13 defines supremum-dense LATTICE6:def 13 :
:: deftheorem Def14 defines infimum-dense LATTICE6:def 14 :
theorem Th23:
theorem Th24:
theorem
:: deftheorem defines MIRRS LATTICE6:def 15 :
:: deftheorem defines JIRRS LATTICE6:def 16 :
theorem
theorem
Lm10:
for L being complete co-noetherian Lattice holds MIRRS L is infimum-dense
Lm11:
for L being complete noetherian Lattice holds JIRRS L is supremum-dense