:: LATTICE7 semantic presentation

definition
let c1 be 1-sorted ;
let c2, c3 be Subset of c1;
redefine pred c= as c2 c= c3 means :: LATTICE7:def 1
for b1 being Element of a1 st b1 in a2 holds
b1 in a3;
compatibility
( c2 c= c3 iff for b1 being Element of c1 st b1 in c2 holds
b1 in c3 )
proof end;
end;

:: deftheorem Def1 defines c= LATTICE7:def 1 :
for b1 being 1-sorted
for b2, b3 being Subset of b1 holds
( b2 c= b3 iff for b4 being Element of b1 st b4 in b2 holds
b4 in b3 );

registration
let c1 be LATTICE;
cluster non empty Element of bool the carrier of a1;
existence
not for b1 being Chain of c1 holds b1 is empty
proof end;
end;

definition
let c1 be LATTICE;
let c2, c3 be Element of c1;
assume E1: c2 <= c3 ;
mode Chain of c2,c3 -> non empty Chain of a1 means :Def2: :: LATTICE7:def 2
( a2 in a4 & a3 in a4 & ( for b1 being Element of a1 st b1 in a4 holds
( a2 <= b1 & b1 <= a3 ) ) );
existence
ex b1 being non empty Chain of c1 st
( c2 in b1 & c3 in b1 & ( for b2 being Element of c1 st b2 in b1 holds
( c2 <= b2 & b2 <= c3 ) ) )
proof end;
end;

:: deftheorem Def2 defines Chain LATTICE7:def 2 :
for b1 being LATTICE
for b2, b3 being Element of b1 st b2 <= b3 holds
for b4 being non empty Chain of b1 holds
( b4 is Chain of b2,b3 iff ( b2 in b4 & b3 in b4 & ( for b5 being Element of b1 st b5 in b4 holds
( b2 <= b5 & b5 <= b3 ) ) ) );

theorem Th1: :: LATTICE7:1
for b1 being LATTICE
for b2, b3 being Element of b1 st b2 <= b3 holds
{b2,b3} is Chain of b2,b3
proof end;

definition
let c1 be finite LATTICE;
let c2 be Element of c1;
func height c2 -> Nat means :Def3: :: LATTICE7:def 3
( ex b1 being Chain of Bottom a1,a2 st a3 = card b1 & ( for b1 being Chain of Bottom a1,a2 holds card b1 <= a3 ) );
existence
ex b1 being Nat st
( ex b2 being Chain of Bottom c1,c2 st b1 = card b2 & ( for b2 being Chain of Bottom c1,c2 holds card b2 <= b1 ) )
proof end;
uniqueness
for b1, b2 being Nat st ex b3 being Chain of Bottom c1,c2 st b1 = card b3 & ( for b3 being Chain of Bottom c1,c2 holds card b3 <= b1 ) & ex b3 being Chain of Bottom c1,c2 st b2 = card b3 & ( for b3 being Chain of Bottom c1,c2 holds card b3 <= b2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines height LATTICE7:def 3 :
for b1 being finite LATTICE
for b2 being Element of b1
for b3 being Nat holds
( b3 = height b2 iff ( ex b4 being Chain of Bottom b1,b2 st b3 = card b4 & ( for b4 being Chain of Bottom b1,b2 holds card b4 <= b3 ) ) );

theorem Th2: :: LATTICE7:2
for b1 being finite LATTICE
for b2, b3 being Element of b1 st b2 < b3 holds
height b2 < height b3
proof end;

theorem Th3: :: LATTICE7:3
for b1 being finite LATTICE
for b2 being Chain of b1
for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
( b3 < b4 iff height b3 < height b4 )
proof end;

theorem Th4: :: LATTICE7:4
for b1 being finite LATTICE
for b2 being Chain of b1
for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
( b3 = b4 iff height b3 = height b4 )
proof end;

theorem Th5: :: LATTICE7:5
for b1 being finite LATTICE
for b2 being Chain of b1
for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
( b3 <= b4 iff height b3 <= height b4 )
proof end;

theorem Th6: :: LATTICE7:6
for b1 being finite LATTICE
for b2 being Element of b1 holds
( height b2 = 1 iff b2 = Bottom b1 )
proof end;

theorem Th7: :: LATTICE7:7
for b1 being non empty finite LATTICE
for b2 being Element of b1 holds height b2 >= 1
proof end;

scheme :: LATTICE7:sch 1
s1{ F1() -> finite LATTICE, P1[ set ] } :
for b1 being Element of F1() holds P1[b1]
provided
E9: for b1 being Element of F1() st ( for b2 being Element of F1() st b2 < b1 holds
P1[b2] ) holds
P1[b1]
proof end;

registration
cluster distributive finite RelStr ;
existence
ex b1 being LATTICE st
( b1 is distributive & b1 is finite )
proof end;
end;

definition
let c1 be LATTICE;
let c2, c3 be Element of c1;
pred c2 <(1) c3 means :Def4: :: LATTICE7:def 4
( a2 < a3 & ( for b1 being Element of a1 holds
( not a2 < b1 or not b1 < a3 ) ) );
end;

:: deftheorem Def4 defines <(1) LATTICE7:def 4 :
for b1 being LATTICE
for b2, b3 being Element of b1 holds
( b2 <(1) b3 iff ( b2 < b3 & ( for b4 being Element of b1 holds
( not b2 < b4 or not b4 < b3 ) ) ) );

theorem Th8: :: LATTICE7:8
for b1 being finite LATTICE
for b2 being non empty Subset of b1 ex b3 being Element of b1 st
( b3 in b2 & ( for b4 being Element of b1 st b4 in b2 holds
not b3 < b4 ) )
proof end;

definition
let c1 be finite LATTICE;
let c2 be non empty Chain of c1;
func max c2 -> Element of a1 means :Def5: :: LATTICE7:def 5
( ( for b1 being Element of a1 st b1 in a2 holds
b1 <= a3 ) & a3 in a2 );
existence
ex b1 being Element of c1 st
( ( for b2 being Element of c1 st b2 in c2 holds
b2 <= b1 ) & b1 in c2 )
proof end;
uniqueness
for b1, b2 being Element of c1 st ( for b3 being Element of c1 st b3 in c2 holds
b3 <= b1 ) & b1 in c2 & ( for b3 being Element of c1 st b3 in c2 holds
b3 <= b2 ) & b2 in c2 holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines max LATTICE7:def 5 :
for b1 being finite LATTICE
for b2 being non empty Chain of b1
for b3 being Element of b1 holds
( b3 = max b2 iff ( ( for b4 being Element of b1 st b4 in b2 holds
b4 <= b3 ) & b3 in b2 ) );

theorem Th9: :: LATTICE7:9
for b1 being finite LATTICE
for b2 being Element of b1 st b2 <> Bottom b1 holds
ex b3 being Element of b1 st b3 <(1) b2
proof end;

definition
let c1 be LATTICE;
func Join-IRR c1 -> Subset of a1 equals :: LATTICE7:def 6
{ b1 where B is Element of a1 : ( b1 <> Bottom a1 & ( for b1, b2 being Element of a1 holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) ) } ;
coherence
{ b1 where B is Element of c1 : ( b1 <> Bottom c1 & ( for b1, b2 being Element of c1 holds
( not b1 = b2 "\/" b3 or b1 = b2 or b1 = b3 ) ) ) } is Subset of c1
proof end;
end;

:: deftheorem Def6 defines Join-IRR LATTICE7:def 6 :
for b1 being LATTICE holds Join-IRR b1 = { b2 where B is Element of b1 : ( b2 <> Bottom b1 & ( for b1, b2 being Element of b1 holds
( not b2 = b3 "\/" b4 or b2 = b3 or b2 = b4 ) ) ) } ;

theorem Th10: :: LATTICE7:10
for b1 being LATTICE
for b2 being Element of b1 holds
( b2 in Join-IRR b1 iff ( b2 <> Bottom b1 & ( for b3, b4 being Element of b1 holds
( not b2 = b3 "\/" b4 or b2 = b3 or b2 = b4 ) ) ) )
proof end;

theorem Th11: :: LATTICE7:11
for b1 being distributive finite LATTICE
for b2 being Element of b1 st b2 in Join-IRR b1 holds
ex b3 being Element of b1 st
( b3 < b2 & ( for b4 being Element of b1 st b4 < b2 holds
b4 <= b3 ) )
proof end;

Lemma15: for b1 being distributive finite LATTICE
for b2 being Element of b1 st ( for b3 being Element of b1 st b3 < b2 holds
sup ((downarrow b3) /\ (Join-IRR b1)) = b3 ) holds
sup ((downarrow b2) /\ (Join-IRR b1)) = b2
proof end;

theorem Th12: :: LATTICE7:12
for b1 being distributive finite LATTICE
for b2 being Element of b1 holds sup ((downarrow b2) /\ (Join-IRR b1)) = b2
proof end;

definition
let c1 be RelStr ;
func LOWER c1 -> non empty set equals :: LATTICE7:def 7
{ b1 where B is Subset of a1 : b1 is lower } ;
coherence
{ b1 where B is Subset of c1 : b1 is lower } is non empty set
proof end;
end;

:: deftheorem Def7 defines LOWER LATTICE7:def 7 :
for b1 being RelStr holds LOWER b1 = { b2 where B is Subset of b1 : b2 is lower } ;

theorem Th13: :: LATTICE7:13
for b1 being distributive finite LATTICE ex b2 being Function of b1,(InclPoset (LOWER (subrelstr (Join-IRR b1)))) st
( b2 is isomorphic & ( for b3 being Element of b1 holds b2 . b3 = (downarrow b3) /\ (Join-IRR b1) ) )
proof end;

theorem Th14: :: LATTICE7:14
for b1 being distributive finite LATTICE holds b1, InclPoset (LOWER (subrelstr (Join-IRR b1))) are_isomorphic
proof end;

definition
mode Ring_of_sets -> set means :Def8: :: LATTICE7:def 8
a1 includes_lattice_of a1;
existence
ex b1 being set st b1 includes_lattice_of b1
proof end;
end;

:: 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 );

registration
cluster non empty Ring_of_sets ;
existence
not for b1 being Ring_of_sets holds b1 is empty
proof end;
end;

Lemma20: for b1, b2 being non empty RelStr
for b3 being Function of b1,b2 st b3 is infs-preserving holds
b3 is meet-preserving
proof end;

Lemma21: for b1, b2 being non empty RelStr
for b3 being Function of b1,b2 st b3 is sups-preserving holds
b3 is join-preserving
proof end;

registration
let c1 be non empty Ring_of_sets ;
cluster InclPoset a1 -> with_suprema with_infima distributive ;
coherence
( InclPoset c1 is with_suprema & InclPoset c1 is with_infima & InclPoset c1 is distributive )
proof end;
end;

theorem Th15: :: LATTICE7:15
for b1 being finite LATTICE holds LOWER (subrelstr (Join-IRR b1)) is Ring_of_sets
proof end;

theorem Th16: :: LATTICE7:16
for b1 being finite LATTICE holds
( b1 is distributive iff ex b2 being non empty Ring_of_sets st b1, InclPoset b2 are_isomorphic )
proof end;