:: by Marek Dudzicz

::

:: Received January 6, 2000

:: Copyright (c) 2000-2021 Association of Mizar Users

definition

let L be 1-sorted ;

let A, B be Subset of L;

( A c= B iff for x being Element of L st x in A holds

x in B ) ;

end;
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 redefine pred A c= B means :: LATTICE7:def 1

for x being Element of L st x in A holds

x in B;

( A c= B iff for x being Element of L st x in A holds

x in B ) ;

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

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

registration
end;

definition

let L be LATTICE;

let x, y be Element of L;

assume A1: x <= y ;

ex b_{1} being non empty Chain of L st

( x in b_{1} & y in b_{1} & ( for z being Element of L st z in b_{1} holds

( x <= z & z <= y ) ) )

end;
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 ( x in it & y in it & ( for z being Element of L st z in it holds

( x <= z & z <= y ) ) );

ex b

( x in b

( x <= z & z <= y ) ) )

proof end;

:: deftheorem Def2 defines Chain LATTICE7:def 2 :

for L being LATTICE

for x, y being Element of L st x <= y holds

for b_{4} being non empty Chain of L holds

( b_{4} is Chain of x,y iff ( x in b_{4} & y in b_{4} & ( for z being Element of L st z in b_{4} holds

( x <= z & z <= y ) ) ) );

for L being LATTICE

for x, y being Element of L st x <= y holds

for b

( b

( x <= z & z <= y ) ) ) );

definition

let L be finite LATTICE;

let x be Element of L;

ex b_{1} being Element of NAT st

( ex A being Chain of Bottom L,x st b_{1} = card A & ( for A being Chain of Bottom L,x holds card A <= b_{1} ) )

for b_{1}, b_{2} being Element of NAT st ex A being Chain of Bottom L,x st b_{1} = card A & ( for A being Chain of Bottom L,x holds card A <= b_{1} ) & ex A being Chain of Bottom L,x st b_{2} = card A & ( for A being Chain of Bottom L,x holds card A <= b_{2} ) holds

b_{1} = b_{2}

end;
let x be Element of L;

func height x -> Element of 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 ( ex A being Chain of Bottom L,x st it = card A & ( for A being Chain of Bottom L,x holds card A <= it ) );

ex b

( ex A being Chain of Bottom L,x st b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3 defines height LATTICE7:def 3 :

for L being finite LATTICE

for x being Element of L

for b_{3} being Element of NAT holds

( b_{3} = height x iff ( ex A being Chain of Bottom L,x st b_{3} = card A & ( for A being Chain of Bottom L,x holds card A <= b_{3} ) ) );

for L being finite LATTICE

for x being Element of L

for b

( b

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 )

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 )

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 )

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;

registration

ex b_{1} being LATTICE st

( b_{1} is distributive & b_{1} is finite )
end;

cluster non empty finite V123() reflexive transitive antisymmetric distributive with_suprema with_infima for RelStr ;

existence ex b

( b

proof end;

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

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

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;

ex b_{1} being Element of L st

( ( for x being Element of L st x in A holds

x <= b_{1} ) & b_{1} in A )

for b_{1}, b_{2} being Element of L st ( for x being Element of L st x in A holds

x <= b_{1} ) & b_{1} in A & ( for x being Element of L st x in A holds

x <= b_{2} ) & b_{2} in A holds

b_{1} = b_{2}

end;
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 ( ( for x being Element of L st x in A holds

x <= it ) & it in A );

ex b

( ( for x being Element of L st x in A holds

x <= b

proof end;

uniqueness for b

x <= b

x <= b

b

proof end;

:: deftheorem Def5 defines max LATTICE7:def 5 :

for L being finite LATTICE

for A being non empty Chain of L

for b_{3} being Element of L holds

( b_{3} = max A iff ( ( for x being Element of L st x in A holds

x <= b_{3} ) & b_{3} in A ) );

for L being finite LATTICE

for A being non empty Chain of L

for b

( b

x <= b

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

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;

{ 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 ) ) ) } is Subset of L

end;
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 { 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 ) ) ) } ;

{ 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 ) ) ) } is Subset of L

proof end;

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

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

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 finite distributive 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 ) )

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 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

proof end;

theorem Th12: :: LATTICE7:12

for L being finite distributive LATTICE

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

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

proof end;

definition
end;

:: deftheorem defines LOWER LATTICE7:def 7 :

for P being RelStr holds LOWER P = { X where X is Subset of P : X is lower } ;

for P being RelStr holds LOWER P = { X where X is Subset of P : X is lower } ;

theorem Th13: :: LATTICE7:13

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

( 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 finite distributive LATTICE holds L, InclPoset (LOWER (subrelstr (Join-IRR L))) are_isomorphic

proof end;

:: deftheorem Def8 defines Ring_of_sets LATTICE7:def 8 :

for b_{1} being set holds

( b_{1} is Ring_of_sets iff b_{1} includes_lattice_of b_{1} );

for b

( b

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

;

registration

let X be non empty Ring_of_sets ;

coherence

( InclPoset X is with_suprema & InclPoset X is with_infima & InclPoset X is distributive )

end;
coherence

( InclPoset X is with_suprema & InclPoset X is with_infima & InclPoset X is distributive )

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 )

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

proof end;