:: LATTICE6 semantic presentation

registration

cluster finite LattStr ;
existence

proof end;

end;

Lemma1: for b₁ being finite Lattice
for b₂ being Subset of b₁ holds
( b₂ is empty or ex b₃ being Element of (LattPOSet b₁) st
( b₃ in b₂ & ( for b₄ being Element of (LattPOSet b₁) st b₄ in b₂ & b₄ <> b₃ holds
not b₄ <= b₃ ) ) )

proof end;

Lemma2: for b₁ being finite Lattice
for b₂ being Subset of b₁ holds
( b₂ is empty or ex b₃ being Element of (LattPOSet b₁) st
( b₃ in b₂ & ( for b₄ being Element of (LattPOSet b₁) st b₄ in b₂ & b₄ <> b₃ holds
not b₃ <= b₄ ) ) )

proof end;

Lemma3: for b₁ being finite Lattice
for b₂ being Subset of b₁ holds
( b₂ is empty or ex b₃ being Element of (LattPOSet b₁) st
for b₄ being Element of (LattPOSet b₁) st b₄ in b₂ holds
b₄ <= b₃ )

proof end;

Lemma4: for b₁ being finite Lattice ex b₂ being Element of (LattPOSet b₁) st
for b₃ being Element of (LattPOSet b₁) holds b₃ <= b₂

proof end;

Lemma5: for b₁ being finite Lattice holds b₁ is complete

proof end;

registration

cluster finite -> complete LattStr ;
coherence by Lemma5;

end;

definition

let c₁ be Lattice;
let c₂ be Subset of c₁;
func c₂ % -> Subset of (LattPOSet a₁) equals :: LATTICE6:def 1
{ (b₁ % ) where B is Element of a₁ : b₁ in a₂ } ;
coherence

proof end;

end;

:: deftheorem Def1 defines % LATTICE6:def 1 :

definition

let c₁ be Lattice;
let c₂ be Subset of (LattPOSet c₁);
func % c₂ -> Subset of a₁ equals :: LATTICE6:def 2
{ (% b₁) where B is Element of (LattPOSet a₁) : b₁ in a₂ } ;
coherence

proof end;

end;

:: deftheorem Def2 defines % LATTICE6:def 2 :

registration

let c₁ be finite Lattice;
cluster LattPOSet a₁ -> well_founded ;
coherence

proof end;

end;

Lemma6: for b₁ being finite Lattice holds (LattPOSet b₁) ~ is well_founded

proof end;

definition

let c₁ be Lattice;
attr a₁ is noetherian means :Def3: :: LATTICE6:def 3
LattPOSet a₁ is well_founded;
attr a₁ is co-noetherian means :Def4: :: LATTICE6:def 4
(LattPOSet a₁) ~ is well_founded;

end;

:: deftheorem Def3 defines noetherian LATTICE6:def 3 :

:: deftheorem Def4 defines co-noetherian LATTICE6:def 4 :

registration

cluster lower-bounded upper-bounded complete noetherian LattStr ;
existence

proof end;

end;

registration

cluster lower-bounded upper-bounded complete co-noetherian LattStr ;
existence

proof end;

end;

theorem Th1: :: LATTICE6:1

for b₁ being Lattice holds
( b₁ is noetherian iff b₁ .: is co-noetherian )

proof end;

Lemma9: for b₁ being finite Lattice holds
( b₁ is noetherian & b₁ is co-noetherian )

proof end;

registration

cluster finite -> noetherian LattStr ;
coherence by Lemma9;
cluster finite -> co-noetherian LattStr ;
coherence by Lemma9;

end;

definition

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
pred c₂ is-upper-neighbour-of c₃ means :Def5: :: LATTICE6:def 5
( a₂ <> a₃ & a₃ [= a₂ & ( for b₁ being Element of a₁ st a₃ [= b₁ & b₁ [= a₂ & not b₁ = a₂ holds
b₁ = a₃ ) );

end;

:: deftheorem Def5 defines is-upper-neighbour-of LATTICE6:def 5 :

notation

let c₁ be Lattice;
let c₂, c₃ be Element of c₁;
synonym c₃ is-lower-neighbour-of c₂ for c₂ is-upper-neighbour-of c₃;

end;

theorem Th2: :: LATTICE6:2

for b₁ being Lattice
for b₂, b₃, b₄ being Element of b₁ st b₃ <> b₄ holds
( ( b₃ is-upper-neighbour-of b₂ & b₄ is-upper-neighbour-of b₂ implies b₂ = b₄ "/\" b₃ ) & ( b₃ is-lower-neighbour-of b₂ & b₄ is-lower-neighbour-of b₂ implies b₂ = b₄ "\/" b₃ ) )

proof end;

theorem Th3: :: LATTICE6:3

for b₁ being noetherian Lattice
for b₂, b₃ being Element of b₁ st b₂ [= b₃ & b₂ <> b₃ holds
ex b₄ being Element of b₁ st
( b₄ [= b₃ & b₄ is-upper-neighbour-of b₂ )

proof end;

theorem Th4: :: LATTICE6:4

for b₁ being co-noetherian Lattice
for b₂, b₃ being Element of b₁ st b₃ [= b₂ & b₂ <> b₃ holds
ex b₄ being Element of b₁ st
( b₃ [= b₄ & b₄ is-lower-neighbour-of b₂ )

proof end;

theorem Th5: :: LATTICE6:5

for b₁ being upper-bounded Lattice
for b₂ being Element of b₁ holds not b₂ is-upper-neighbour-of Top b₁

proof end;

theorem Th6: :: LATTICE6:6

for b₁ being upper-bounded noetherian Lattice
for b₂ being Element of b₁ holds
( b₂ = Top b₁ iff for b₃ being Element of b₁ holds not b₃ is-upper-neighbour-of b₂ )

proof end;

theorem Th7: :: LATTICE6:7

for b₁ being lower-bounded Lattice
for b₂ being Element of b₁ holds not b₂ is-lower-neighbour-of Bottom b₁

proof end;

theorem Th8: :: LATTICE6:8

for b₁ being lower-bounded co-noetherian Lattice
for b₂ being Element of b₁ holds
( b₂ = Bottom b₁ iff for b₃ being Element of b₁ holds not b₃ is-lower-neighbour-of b₂ )

proof end;

definition

let c₁ be complete Lattice;
let c₂ be Element of c₁;
func c₂ *' -> Element of a₁ equals :: LATTICE6:def 6
"/\" { b₁ where B is Element of a₁ : ( a₂ [= b₁ & b₁ <> a₂ ) } ,a₁;
correctness ;
func *' c₂ -> Element of a₁ equals :: LATTICE6:def 7
"\/" { b₁ where B is Element of a₁ : ( b₁ [= a₂ & b₁ <> a₂ ) } ,a₁;
correctness ;

end;

:: deftheorem Def6 defines *' LATTICE6:def 6 :

:: deftheorem Def7 defines *' LATTICE6:def 7 :

definition

let c₁ be complete Lattice;
let c₂ be Element of c₁;
attr a₂ is completely-meet-irreducible means :Def8: :: LATTICE6:def 8
a₂ *' <> a₂;
attr a₂ is completely-join-irreducible means :Def9: :: LATTICE6:def 9
*' a₂ <> a₂;

end;

:: deftheorem Def8 defines completely-meet-irreducible LATTICE6:def 8 :

:: deftheorem Def9 defines completely-join-irreducible LATTICE6:def 9 :

theorem Th9: :: LATTICE6:9

for b₁ being complete Lattice
for b₂ being Element of b₁ holds
( b₂ [= b₂ *' & *' b₂ [= b₂ )

proof end;

theorem Th10: :: LATTICE6:10

for b₁ being complete Lattice holds
( (Top b₁) *' = Top b₁ & (Top b₁) % is meet-irreducible )

proof end;

theorem Th11: :: LATTICE6:11

for b₁ being complete Lattice holds
( *' (Bottom b₁) = Bottom b₁ & (Bottom b₁) % is join-irreducible )

proof end;

theorem Th12: :: LATTICE6:12

for b₁ being complete Lattice
for b₂ being Element of b₁ st b₂ is completely-meet-irreducible holds
( b₂ *' is-upper-neighbour-of b₂ & ( for b₃ being Element of b₁ st b₃ is-upper-neighbour-of b₂ holds
b₃ = b₂ *' ) )

proof end;

theorem Th13: :: LATTICE6:13

for b₁ being complete Lattice
for b₂ being Element of b₁ st b₂ is completely-join-irreducible holds
( *' b₂ is-lower-neighbour-of b₂ & ( for b₃ being Element of b₁ st b₃ is-lower-neighbour-of b₂ holds
b₃ = *' b₂ ) )

proof end;

theorem Th14: :: LATTICE6:14

for b₁ being complete noetherian Lattice
for b₂ being Element of b₁ holds
( b₂ is completely-meet-irreducible iff ex b₃ being Element of b₁ st
( b₃ is-upper-neighbour-of b₂ & ( for b₄ being Element of b₁ st b₄ is-upper-neighbour-of b₂ holds
b₄ = b₃ ) ) )

proof end;

theorem Th15: :: LATTICE6:15

for b₁ being complete co-noetherian Lattice
for b₂ being Element of b₁ holds
( b₂ is completely-join-irreducible iff ex b₃ being Element of b₁ st
( b₃ is-lower-neighbour-of b₂ & ( for b₄ being Element of b₁ st b₄ is-lower-neighbour-of b₂ holds
b₄ = b₃ ) ) )

proof end;

theorem Th16: :: LATTICE6:16

for b₁ being complete Lattice
for b₂ being Element of b₁ st b₂ is completely-meet-irreducible holds
b₂ % is meet-irreducible

proof end;

Lemma26: for b₁ being Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ "/\" b₃ = (b₂ % ) "/\" (b₃ % ) & b₂ "\/" b₃ = (b₂ % ) "\/" (b₃ % ) )

proof end;

theorem Th17: :: LATTICE6:17

for b₁ being complete noetherian Lattice
for b₂ being Element of b₁ st b₂ <> Top b₁ holds
( b₂ is completely-meet-irreducible iff b₂ % is meet-irreducible )

proof end;

theorem Th18: :: LATTICE6:18

for b₁ being complete Lattice
for b₂ being Element of b₁ st b₂ is completely-join-irreducible holds
b₂ % is join-irreducible

proof end;

theorem Th19: :: LATTICE6:19

for b₁ being complete co-noetherian Lattice
for b₂ being Element of b₁ st b₂ <> Bottom b₁ holds
( b₂ is completely-join-irreducible iff b₂ % is join-irreducible )

proof end;

theorem Th20: :: LATTICE6:20

for b₁ being finite Lattice
for b₂ being Element of b₁ st b₂ <> Bottom b₁ & b₂ <> Top b₁ holds
( ( b₂ is completely-meet-irreducible implies b₂ % is meet-irreducible ) & ( b₂ % is meet-irreducible implies b₂ is completely-meet-irreducible ) & ( b₂ is completely-join-irreducible implies b₂ % is join-irreducible ) & ( b₂ % is join-irreducible implies b₂ is completely-join-irreducible ) ) by Th17, Th19;

definition

let c₁ be Lattice;
let c₂ be Element of c₁;
attr a₂ is atomic means :Def10: :: LATTICE6:def 10
a₂ is-upper-neighbour-of Bottom a₁;
attr a₂ is co-atomic means :Def11: :: LATTICE6:def 11
a₂ is-lower-neighbour-of Top a₁;

end;

:: deftheorem Def10 defines atomic LATTICE6:def 10 :

:: deftheorem Def11 defines co-atomic LATTICE6:def 11 :

theorem Th21: :: LATTICE6:21

for b₁ being complete Lattice
for b₂ being Element of b₁ st b₂ is atomic holds
b₂ is completely-join-irreducible

proof end;

theorem Th22: :: LATTICE6:22

for b₁ being complete Lattice
for b₂ being Element of b₁ st b₂ is co-atomic holds
b₂ is completely-meet-irreducible

proof end;

definition

let c₁ be Lattice;
attr a₁ is atomic means :Def12: :: LATTICE6:def 12
for b₁ being Element of a₁ ex b₂ being Subset of a₁ st
( ( for b₃ being Element of a₁ st b₃ in b₂ holds
b₃ is atomic ) & b₁ = "\/" b₂,a₁ );

end;

:: deftheorem Def12 defines atomic LATTICE6:def 12 :

registration

cluster strict trivial LattStr ;
existence

proof end;

end;

Lemma33: ex b₁ being Lattice st
( b₁ is atomic & b₁ is complete )

proof end;

registration

cluster complete atomic LattStr ;
existence by Lemma33;

end;

definition

let c₁ be complete Lattice;
let c₂ be Subset of c₁;
attr a₂ is supremum-dense means :Def13: :: LATTICE6:def 13
for b₁ being Element of a₁ ex b₂ being Subset of a₂ st b₁ = "\/" b₂,a₁;
attr a₂ is infimum-dense means :Def14: :: LATTICE6:def 14
for b₁ being Element of a₁ ex b₂ being Subset of a₂ st b₁ = "/\" b₂,a₁;

end;

:: deftheorem Def13 defines supremum-dense LATTICE6:def 13 :

:: deftheorem Def14 defines infimum-dense LATTICE6:def 14 :

theorem Th23: :: LATTICE6:23

for b₁ being complete Lattice
for b₂ being Subset of b₁ holds
( b₂ is supremum-dense iff for b₃ being Element of b₁ holds b₃ = "\/" { b₄ where B is Element of b₁ : ( b₄ in b₂ & b₄ [= b₃ ) } ,b₁ )

proof end;

theorem Th24: :: LATTICE6:24

for b₁ being complete Lattice
for b₂ being Subset of b₁ holds
( b₂ is infimum-dense iff for b₃ being Element of b₁ holds b₃ = "/\" { b₄ where B is Element of b₁ : ( b₄ in b₂ & b₃ [= b₄ ) } ,b₁ )

proof end;

theorem Th25: :: LATTICE6:25

for b₁ being complete Lattice
for b₂ being Subset of b₁ holds
( b₂ is infimum-dense iff b₂ % is order-generating )

proof end;

definition

let c₁ be complete Lattice;
func MIRRS c₁ -> Subset of a₁ equals :: LATTICE6:def 15
{ b₁ where B is Element of a₁ : b₁ is completely-meet-irreducible } ;
correctness

proof end;

func JIRRS c₁ -> Subset of a₁ equals :: LATTICE6:def 16
{ b₁ where B is Element of a₁ : b₁ is completely-join-irreducible } ;
correctness

proof end;

end;

:: deftheorem Def15 defines MIRRS LATTICE6:def 15 :

:: deftheorem Def16 defines JIRRS LATTICE6:def 16 :

theorem Th26: :: LATTICE6:26

for b₁ being complete Lattice
for b₂ being Subset of b₁ st b₂ is supremum-dense holds
JIRRS b₁ c= b₂

proof end;

theorem Th27: :: LATTICE6:27

for b₁ being complete Lattice
for b₂ being Subset of b₁ st b₂ is infimum-dense holds
MIRRS b₁ c= b₂

proof end;

Lemma38: for b₁ being complete co-noetherian Lattice holds MIRRS b₁ is infimum-dense

proof end;

registration

let c₁ be complete co-noetherian Lattice;
cluster MIRRS a₁ -> infimum-dense ;
coherence by Lemma38;

end;

Lemma39: for b₁ being complete noetherian Lattice holds JIRRS b₁ is supremum-dense

proof end;

registration

let c₁ be complete noetherian Lattice;
cluster JIRRS a₁ -> supremum-dense ;
coherence by Lemma39;

end;