:: On the Characterization of Modular and Distributive Lattices
:: by Adam Naumowicz
::
:: Received April 3, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users

:: Preliminaries

theorem :: YELLOW11:1

3 = {0,1,2} by CARD_1:51;

theorem Th2: :: YELLOW11:2

2 \ 1 = {1}

proof end;

theorem Th3: :: YELLOW11:3

3 \ 1 = {1,2}

proof end;

theorem Th4: :: YELLOW11:4

3 \ 2 = {2}

proof end;

Lm1: 3 \ 2 c= 3 \ 1

proof end;

theorem Th5: :: YELLOW11:5

for L being reflexive antisymmetric with_suprema with_infima RelStr
for a, b being Element of L holds
( a "/\" b = b iff a "\/" b = a )

proof end;

theorem Th6: :: YELLOW11:6

for L being LATTICE
for a, b, c being Element of L holds (a "/\" b) "\/" (a "/\" c) <= a "/\" (b "\/" c)

proof end;

theorem Th7: :: YELLOW11:7

for L being LATTICE
for a, b, c being Element of L holds a "\/" (b "/\" c) <= (a "\/" b) "/\" (a "\/" c)

proof end;

theorem Th8: :: YELLOW11:8

for L being LATTICE
for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) <= (a "\/" b) "/\" c

proof end;

definition

func N_5 -> RelStr equals :: YELLOW11:def 1
InclPoset {0,(3 \ 1),2,(3 \ 2),3};

correctness
coherence
InclPoset {0,(3 \ 1),2,(3 \ 2),3} is RelStr ;
;

end;

:: deftheorem defines N_5 YELLOW11:def 1 :
N_5 = InclPoset {0,(3 \ 1),2,(3 \ 2),3};

registration

cluster N_5 -> strict reflexive transitive antisymmetric ;

correctness
coherence
( N_5 is strict & N_5 is reflexive & N_5 is transitive & N_5 is antisymmetric );
;

cluster N_5 -> with_suprema with_infima ;

correctness
coherence
( N_5 is with_infima & N_5 is with_suprema );

proof end;

end;

definition

func M_3 -> RelStr equals :: YELLOW11:def 2
InclPoset {0,1,(2 \ 1),(3 \ 2),3};

correctness
coherence
InclPoset {0,1,(2 \ 1),(3 \ 2),3} is RelStr ;
;

end;

:: deftheorem defines M_3 YELLOW11:def 2 :
M_3 = InclPoset {0,1,(2 \ 1),(3 \ 2),3};

registration

cluster M_3 -> strict reflexive transitive antisymmetric ;

correctness
coherence
( M_3 is strict & M_3 is reflexive & M_3 is transitive & M_3 is antisymmetric );
;

cluster M_3 -> with_suprema with_infima ;

correctness
coherence
( M_3 is with_infima & M_3 is with_suprema );

proof end;

end;

theorem Th9: :: YELLOW11:9

for L being LATTICE holds
( ex K being full Sublattice of L st N_5 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st
( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = b & c "/\" d = a & b "\/" c = e & c "\/" d = e ) )

proof end;

theorem Th10: :: YELLOW11:10

for L being LATTICE holds
( ex K being full Sublattice of L st M_3 ,K are_isomorphic iff ex a, b, c, d, e being Element of L st
( a,b,c,d,e are_mutually_distinct & a "/\" b = a & a "/\" c = a & a "/\" d = a & b "/\" e = b & c "/\" e = c & d "/\" e = d & b "/\" c = a & b "/\" d = a & c "/\" d = a & b "\/" c = e & b "\/" d = e & c "\/" d = e ) )

proof end;

definition

let L be non empty RelStr ;

attr L is modular means :: YELLOW11:def 3
for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c;

end;

:: deftheorem defines modular YELLOW11:def 3 :
for L being non empty RelStr holds
( L is modular iff for a, b, c being Element of L st a <= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c );

registration

cluster non empty reflexive antisymmetric with_infima distributive -> non empty reflexive antisymmetric with_infima modular for RelStr ;

coherence
for b₁ being non empty reflexive antisymmetric with_infima RelStr st b₁ is distributive holds
b₁ is modular

proof end;

end;

Lm2: for L being LATTICE holds
( L is modular iff for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct or not a "/\" b = a or not a "/\" c = a or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = b or not c "/\" d = a or not b "\/" c = e or not c "\/" d = e ) )

proof end;

theorem :: YELLOW11:11

for L being LATTICE holds
( L is modular iff for K being full Sublattice of L holds not N_5 ,K are_isomorphic )

proof end;

Lm3: for L being LATTICE st L is modular holds
( L is distributive iff for a, b, c, d, e being Element of L holds
( not a,b,c,d,e are_mutually_distinct or not a "/\" b = a or not a "/\" c = a or not a "/\" d = a or not b "/\" e = b or not c "/\" e = c or not d "/\" e = d or not b "/\" c = a or not b "/\" d = a or not c "/\" d = a or not b "\/" c = e or not b "\/" d = e or not c "\/" d = e ) )

proof end;

theorem :: YELLOW11:12

for L being LATTICE st L is modular holds
( L is distributive iff for K being full Sublattice of L holds not M_3 ,K are_isomorphic )

proof end;

definition

let L be non empty RelStr ;
let a, b be Element of L;

func [#a,b#] -> Subset of L means :Def4: :: YELLOW11:def 4
for c being Element of L holds
( c in it iff ( a <= c & c <= b ) );

existence
ex b₁ being Subset of L st
for c being Element of L holds
( c in b₁ iff ( a <= c & c <= b ) )

proof end;

uniqueness
for b₁, b₂ being Subset of L st ( for c being Element of L holds
( c in b₁ iff ( a <= c & c <= b ) ) ) & ( for c being Element of L holds
( c in b₂ iff ( a <= c & c <= b ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines [# YELLOW11:def 4 :
for L being non empty RelStr
for a, b being Element of L
for b₄ being Subset of L holds
( b₄ = [#a,b#] iff for c being Element of L holds
( c in b₄ iff ( a <= c & c <= b ) ) );

definition

let L be non empty RelStr ;
let IT be Subset of L;

attr IT is interval means :: YELLOW11:def 5
ex a, b being Element of L st IT = [#a,b#];

end;

:: deftheorem defines interval YELLOW11:def 5 :
for L being non empty RelStr
for IT being Subset of L holds
( IT is interval iff ex a, b being Element of L st IT = [#a,b#] );

registration

let L be non empty reflexive transitive RelStr ;

cluster non empty interval -> directed for Element of bool the carrier of L;

coherence
for b₁ being Subset of L st not b₁ is empty & b₁ is interval holds
b₁ is directed

proof end;

cluster non empty interval -> filtered for Element of bool the carrier of L;

coherence
for b₁ being Subset of L st not b₁ is empty & b₁ is interval holds
b₁ is filtered

proof end;

end;

registration

let L be non empty RelStr ;
let a, b be Element of L;

cluster [#a,b#] -> interval ;

coherence
[#a,b#] is interval ;

end;

theorem :: YELLOW11:13

for L being non empty reflexive transitive RelStr
for a, b being Element of L holds [#a,b#] = (uparrow a) /\ (downarrow b)

proof end;

registration

let L be with_infima Poset;
let a, b be Element of L;

cluster subrelstr [#a,b#] -> meet-inheriting ;

coherence
subrelstr [#a,b#] is meet-inheriting

proof end;

end;

registration

let L be with_suprema Poset;
let a, b be Element of L;

cluster subrelstr [#a,b#] -> join-inheriting ;

coherence
subrelstr [#a,b#] is join-inheriting

proof end;

end;

theorem :: YELLOW11:14

for L being LATTICE
for a, b being Element of L st L is modular holds
subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic

proof end;

registration

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

existence
ex b₁ being LATTICE st
( b₁ is finite & not b₁ is empty )

proof end;

end;

registration

cluster finite reflexive transitive antisymmetric with_infima -> lower-bounded for RelStr ;

coherence
for b₁ being Semilattice st b₁ is finite holds
b₁ is lower-bounded

proof end;

end;

registration

cluster finite reflexive transitive antisymmetric with_suprema with_infima -> complete for RelStr ;

coherence
for b₁ being LATTICE st b₁ is finite holds
b₁ is complete

proof end;

end;