begin
:: deftheorem defines c= LATTICE7:def 1 :
for L being 1-sorted
for A, B being Subset of L holds
( A c= B iff for x being Element of L st x in A holds
x in B );
:: deftheorem Def2 defines Chain LATTICE7:def 2 :
for L being LATTICE
for x, y being Element of L st x <= y holds
for b4 being non empty Chain of L holds
( b4 is Chain of x,y iff ( x in b4 & y in b4 & ( for z being Element of L st z in b4 holds
( x <= z & z <= y ) ) ) );
theorem Th1:
:: deftheorem Def3 defines height LATTICE7:def 3 :
for L being finite LATTICE
for x being Element of L
for b3 being Element of NAT holds
( b3 = height x iff ( ex A being Chain of Bottom L,x st b3 = card A & ( for A being Chain of Bottom L,x holds card A <= b3 ) ) );
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem
theorem Th7:
begin
:: deftheorem Def4 defines <(1) LATTICE7:def 4 :
for L being LATTICE
for x, y being Element of L holds
( x <(1) y iff ( x < y & ( for z being Element of L holds
( not x < z or not z < y ) ) ) );
theorem Th8:
:: deftheorem Def5 defines max LATTICE7:def 5 :
for L being finite LATTICE
for A being non empty Chain of L
for b3 being Element of L holds
( b3 = max A iff ( ( for x being Element of L st x in A holds
x <= b3 ) & b3 in A ) );
theorem Th9:
:: deftheorem defines Join-IRR LATTICE7:def 6 :
for L being LATTICE holds Join-IRR L = { a where a is Element of L : ( a <> Bottom L & ( for b, c being Element of L holds
( not a = b "\/" c or a = b or a = c ) ) ) } ;
theorem Th10:
theorem Th11:
Lm1:
for L being finite distributive LATTICE
for a being Element of L st ( for b being Element of L st b < a holds
sup ((downarrow b) /\ (Join-IRR L)) = b ) holds
sup ((downarrow a) /\ (Join-IRR L)) = a
theorem Th12:
begin
:: deftheorem defines LOWER LATTICE7:def 7 :
for P being RelStr holds LOWER P = { X where X is Subset of P : X is lower } ;
theorem Th13:
theorem Th14:
:: deftheorem Def8 defines Ring_of_sets LATTICE7:def 8 :
for b1 being set holds
( b1 is Ring_of_sets iff b1 includes_lattice_of b1 );
Lm2:
for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is infs-preserving holds
f is meet-preserving
Lm3:
for L1, L2 being non empty RelStr
for f being Function of L1,L2 st f is sups-preserving holds
f is join-preserving
theorem Th15:
theorem