:: LATTICE7 semantic presentation

definition

let L be 1-sorted ;
let A, B be Subset of L;
:: original: c=
redefine pred A c= B means :: LATTICE7:def 1
for x being Element of L st x in A holds
x in B;
compatibility

proof end;

end;

:: deftheorem defines c= LATTICE7:def 1 :

registration

let L be LATTICE;
cluster non empty Element of bool the carrier of L;
existence

proof end;

end;

definition

let L be LATTICE;
let x, y be Element of L;
assume A1: x <= y ;
mode Chain of x,y -> non empty Chain of L means :Def2: :: LATTICE7:def 2
( x in it & y in it & ( for z being Element of L st z in it holds
( x <= z & z <= y ) ) );
existence

proof end;

end;

:: deftheorem Def2 defines Chain LATTICE7:def 2 :

theorem Th1: :: LATTICE7:1

for L being LATTICE
for x, y being Element of L st x <= y holds
{x,y} is Chain of x,y

proof end;

definition

let L be finite LATTICE;
let x be Element of L;
func height x -> Nat means :Def3: :: LATTICE7:def 3
( ex A being Chain of Bottom L,x st it = card A & ( for A being Chain of Bottom L,x holds card A <= it ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines height LATTICE7:def 3 :

theorem Th2: :: LATTICE7:2

for L being finite LATTICE
for a, b being Element of L st a < b holds
height a < height b

proof end;

theorem Th3: :: LATTICE7:3

for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x < y iff height x < height y )

proof end;

theorem Th4: :: LATTICE7:4

for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x = y iff height x = height y )

proof end;

theorem Th5: :: LATTICE7:5

for L being finite LATTICE
for C being Chain of L
for x, y being Element of L st x in C & y in C holds
( x <= y iff height x <= height y )

proof end;

theorem :: LATTICE7:6

for L being finite LATTICE
for x being Element of L holds
( height x = 1 iff x = Bottom L )

proof end;

theorem Th7: :: LATTICE7:7

for L being non empty finite LATTICE
for x being Element of L holds height x >= 1

proof end;

scheme :: LATTICE7:sch 1
LattInd{ F₁() -> finite LATTICE, P₁[ set ] } :

for x being Element of F₁() holds P₁[x]

provided

A1: for x being Element of F₁() st ( for b being Element of F₁() st b < x holds
P₁[b] ) holds
P₁[x]

proof end;

registration

cluster distributive finite RelStr ;
existence

proof end;

end;

definition

let L be LATTICE;
let x, y be Element of L;
pred x <(1) y means :Def4: :: LATTICE7:def 4
( x < y & ( for z being Element of L holds
( not x < z or not z < y ) ) );

end;

:: deftheorem Def4 defines <(1) LATTICE7:def 4 :

theorem Th8: :: LATTICE7:8

for L being finite LATTICE
for X being non empty Subset of L ex x being Element of L st
( x in X & ( for y being Element of L st y in X holds
not x < y ) )

proof end;

definition

let L be finite LATTICE;
let A be non empty Chain of L;
func max A -> Element of L means :Def5: :: LATTICE7:def 5
( ( for x being Element of L st x in A holds
x <= it ) & it in A );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines max LATTICE7:def 5 :

theorem Th9: :: LATTICE7:9

for L being finite LATTICE
for y being Element of L st y <> Bottom L holds
ex x being Element of L st x <(1) y

proof end;

definition

let L be LATTICE;
func Join-IRR L -> Subset of L equals :: LATTICE7:def 6
{ 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 ) ) ) } ;
coherence

proof end;

end;

:: deftheorem defines Join-IRR LATTICE7:def 6 :

theorem Th10: :: LATTICE7:10

for L being LATTICE
for x being Element of L holds
( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds
( not x = b "\/" c or x = b or x = c ) ) ) )

proof end;

theorem Th11: :: LATTICE7:11

for L being distributive finite LATTICE
for x being Element of L st x in Join-IRR L holds
ex z being Element of L st
( z < x & ( for y being Element of L st y < x holds
y <= z ) )

proof end;

Lm1: for L being distributive finite 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

proof end;

theorem Th12: :: LATTICE7:12

for L being distributive finite LATTICE
for x being Element of L holds sup ((downarrow x) /\ (Join-IRR L)) = x

proof end;

definition

let P be RelStr ;
func LOWER P -> non empty set equals :: LATTICE7:def 7
{ X where X is Subset of P : X is lower } ;
coherence

proof end;

end;

:: deftheorem defines LOWER LATTICE7:def 7 :

theorem Th13: :: LATTICE7:13

for L being distributive finite LATTICE ex r being Function of L,(InclPoset (LOWER (subrelstr (Join-IRR L)))) st
( r is isomorphic & ( for a being Element of L holds r . a = (downarrow a) /\ (Join-IRR L) ) )

proof end;

theorem Th14: :: LATTICE7:14

for L being distributive finite LATTICE holds L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic

proof end;

definition

mode Ring_of_sets -> set means :Def8: :: LATTICE7:def 8
it includes_lattice_of it;
existence

proof end;

end;

:: deftheorem Def8 defines Ring_of_sets LATTICE7:def 8 :

registration

cluster non empty Ring_of_sets ;
existence

proof end;

end;

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

proof end;

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

proof end;

registration

let X be non empty Ring_of_sets ;
cluster InclPoset X -> with_suprema with_infima distributive ;
coherence

proof end;

end;

theorem Th15: :: LATTICE7:15

for L being finite LATTICE holds LOWER (subrelstr (Join-IRR L)) is Ring_of_sets

proof end;

theorem :: LATTICE7:16

for L being finite LATTICE holds
( L is distributive iff ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic )

proof end;