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 :
for L being Lattice
for D being Subset of L holds D % = { (d % ) where d is Element of L : d in D } ;
:: deftheorem defines % LATTICE6:def 2 :
for L being Lattice
for D being Subset of (LattPOSet L) holds % D = { (% d) where d is Element of (LattPOSet L) : d in D } ;
Lm6:
for L being finite Lattice holds (LattPOSet L) ~ is well_founded
:: deftheorem Def3 defines noetherian LATTICE6:def 3 :
for L being Lattice holds
( L is noetherian iff LattPOSet L is well_founded );
:: deftheorem Def4 defines co-noetherian LATTICE6:def 4 :
for L being Lattice holds
( L is co-noetherian iff (LattPOSet L) ~ is well_founded );
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 :
for L being Lattice
for a, b being Element of L holds
( a is-upper-neighbour-of b iff ( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds
c = b ) ) );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
:: deftheorem defines *' LATTICE6:def 6 :
for L being complete Lattice
for a being Element of L holds a *' = "/\" { d where d is Element of L : ( a [= d & d <> a ) } ,L;
:: deftheorem defines *' LATTICE6:def 7 :
for L being complete Lattice
for a being Element of L holds *' a = "\/" { d where d is Element of L : ( d [= a & d <> a ) } ,L;
:: deftheorem Def8 defines completely-meet-irreducible LATTICE6:def 8 :
for L being complete Lattice
for a being Element of L holds
( a is completely-meet-irreducible iff a *' <> a );
:: deftheorem Def9 defines completely-join-irreducible LATTICE6:def 9 :
for L being complete Lattice
for a being Element of L holds
( a is completely-join-irreducible iff *' a <> a );
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 :
for L being Lattice
for a being Element of L holds
( a is atomic iff a is-upper-neighbour-of Bottom L );
:: deftheorem Def11 defines co-atomic LATTICE6:def 11 :
for L being Lattice
for a being Element of L holds
( a is co-atomic iff a is-lower-neighbour-of Top L );
theorem
theorem
:: deftheorem Def12 defines atomic LATTICE6:def 12 :
for L being Lattice holds
( L is atomic iff for a being Element of L ex X being Subset of L st
( ( for x being Element of L st x in X holds
x is atomic ) & a = "\/" X,L ) );
Lm9:
ex L being Lattice st
( L is atomic & L is complete )
:: deftheorem Def13 defines supremum-dense LATTICE6:def 13 :
for L being complete Lattice
for D being Subset of L holds
( D is supremum-dense iff for a being Element of L ex D9 being Subset of D st a = "\/" D9,L );
:: deftheorem Def14 defines infimum-dense LATTICE6:def 14 :
for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L ex D9 being Subset of D st a = "/\" D9,L );
theorem Th23:
theorem Th24:
theorem
:: deftheorem defines MIRRS LATTICE6:def 15 :
for L being complete Lattice holds MIRRS L = { a where a is Element of L : a is completely-meet-irreducible } ;
:: deftheorem defines JIRRS LATTICE6:def 16 :
for L being complete Lattice holds JIRRS L = { a where a is Element of L : a is completely-join-irreducible } ;
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