:: LATTICE6 semantic presentation

registration

cluster finite LattStr ;
existence

proof end;

end;

Lm1: for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not b <= a ) ) )

proof end;

Lm2: for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
( a in X & ( for b being Element of (LattPOSet L) st b in X & b <> a holds
not a <= b ) ) )

proof end;

Lm3: for L being finite Lattice
for X being Subset of L holds
( X is empty or ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) st b in X holds
b <= a )

proof end;

Lm4: for L being finite Lattice ex a being Element of (LattPOSet L) st
for b being Element of (LattPOSet L) holds b <= a

proof end;

Lm5: for L being finite Lattice holds L is complete

proof end;

registration

cluster finite -> complete LattStr ;
coherence by Lm5;

end;

definition

let L be Lattice;
let D be Subset of L;
func D % -> Subset of (LattPOSet L) equals :: LATTICE6:def 1
{ (d % ) where d is Element of L : d in D } ;
coherence

proof end;

end;

:: deftheorem defines % LATTICE6:def 1 :

definition

let L be Lattice;
let D be Subset of (LattPOSet L);
func % D -> Subset of L equals :: LATTICE6:def 2
{ (% d) where d is Element of (LattPOSet L) : d in D } ;
coherence

proof end;

end;

:: deftheorem defines % LATTICE6:def 2 :

registration

let L be finite Lattice;
cluster LattPOSet L -> well_founded ;
coherence

proof end;

end;

Lm6: for L being finite Lattice holds (LattPOSet L) ~ is well_founded

proof end;

definition

let L be Lattice;
attr L is noetherian means :Def3: :: LATTICE6:def 3
LattPOSet L is well_founded;
attr L is co-noetherian means :Def4: :: LATTICE6:def 4
(LattPOSet L) ~ 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 :: LATTICE6:1

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

proof end;

Lm7: for L being finite Lattice holds
( L is noetherian & L is co-noetherian )

proof end;

registration

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

end;

definition

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

end;

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

notation

let L be Lattice;
let a, b be Element of L;
synonym b is-lower-neighbour-of a for a is-upper-neighbour-of b;

end;

theorem Th2: :: LATTICE6:2

for L being Lattice
for a, b, c being Element of L st b <> c holds
( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )

proof end;

theorem Th3: :: LATTICE6:3

for L being noetherian Lattice
for a, d being Element of L st a [= d & a <> d holds
ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )

proof end;

theorem Th4: :: LATTICE6:4

for L being co-noetherian Lattice
for a, d being Element of L st d [= a & a <> d holds
ex c being Element of L st
( d [= c & c is-lower-neighbour-of a )

proof end;

theorem Th5: :: LATTICE6:5

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

proof end;

theorem Th6: :: LATTICE6:6

for L being upper-bounded noetherian Lattice
for a being Element of L holds
( a = Top L iff for b being Element of L holds not b is-upper-neighbour-of a )

proof end;

theorem Th7: :: LATTICE6:7

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

proof end;

theorem Th8: :: LATTICE6:8

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

proof end;

definition

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

end;

:: deftheorem defines *' LATTICE6:def 6 :

:: deftheorem defines *' LATTICE6:def 7 :

definition

let L be complete Lattice;
let a be Element of L;
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 L being complete Lattice
for a being Element of L holds
( a [= a *' & *' a [= a )

proof end;

theorem :: LATTICE6:10

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

proof end;

theorem :: LATTICE6:11

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

proof end;

theorem Th12: :: LATTICE6:12

for L being complete Lattice
for a being Element of L st a is completely-meet-irreducible holds
( a *' is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = a *' ) )

proof end;

theorem Th13: :: LATTICE6:13

for L being complete Lattice
for a being Element of L st a is completely-join-irreducible holds
( *' a is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = *' a ) )

proof end;

theorem Th14: :: LATTICE6:14

for L being complete noetherian Lattice
for a being Element of L holds
( a is completely-meet-irreducible iff ex b being Element of L st
( b is-upper-neighbour-of a & ( for c being Element of L st c is-upper-neighbour-of a holds
c = b ) ) )

proof end;

theorem Th15: :: LATTICE6:15

for L being complete co-noetherian Lattice
for a being Element of L holds
( a is completely-join-irreducible iff ex b being Element of L st
( b is-lower-neighbour-of a & ( for c being Element of L st c is-lower-neighbour-of a holds
c = b ) ) )

proof end;

theorem Th16: :: LATTICE6:16

for L being complete Lattice
for a being Element of L st a is completely-meet-irreducible holds
a % is meet-irreducible

proof end;

Lm8: for L being Lattice
for a, b being Element of L holds
( a "/\" b = (a % ) "/\" (b % ) & a "\/" b = (a % ) "\/" (b % ) )

proof end;

theorem Th17: :: LATTICE6:17

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

proof end;

theorem Th18: :: LATTICE6:18

for L being complete Lattice
for a being Element of L st a is completely-join-irreducible holds
a % is join-irreducible

proof end;

theorem Th19: :: LATTICE6:19

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

proof end;

theorem :: LATTICE6:20

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

definition

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

end;

:: deftheorem Def10 defines atomic LATTICE6:def 10 :

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

theorem :: LATTICE6:21

for L being complete Lattice
for a being Element of L st a is atomic holds
a is completely-join-irreducible

proof end;

theorem :: LATTICE6:22

for L being complete Lattice
for a being Element of L st a is co-atomic holds
a is completely-meet-irreducible

proof end;

definition

let L be Lattice;
attr L is atomic means :Def12: :: LATTICE6:def 12
for a being Element of L ex X being Subset of L st
( ( for x being Element of L st x in X holds
x is atomic ) & a = "\/" X,L );

end;

:: deftheorem Def12 defines atomic LATTICE6:def 12 :

registration

cluster strict trivial LattStr ;
existence

proof end;

end;

Lm9: ex L being Lattice st
( L is atomic & L is complete )

proof end;

registration

cluster complete atomic LattStr ;
existence by Lm9;

end;

definition

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

end;

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

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

theorem Th23: :: LATTICE6:23

for L being complete Lattice
for D being Subset of L holds
( D is supremum-dense iff for a being Element of L holds a = "\/" { d where d is Element of L : ( d in D & d [= a ) } ,L )

proof end;

theorem Th24: :: LATTICE6:24

for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L holds a = "/\" { d where d is Element of L : ( d in D & a [= d ) } ,L )

proof end;

theorem :: LATTICE6:25

for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff D % is order-generating )

proof end;

definition

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

proof end;

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

proof end;

end;

:: deftheorem defines MIRRS LATTICE6:def 15 :

:: deftheorem defines JIRRS LATTICE6:def 16 :

theorem :: LATTICE6:26

for L being complete Lattice
for D being Subset of L st D is supremum-dense holds
JIRRS L c= D

proof end;

theorem :: LATTICE6:27

for L being complete Lattice
for D being Subset of L st D is infimum-dense holds
MIRRS L c= D

proof end;

Lm10: for L being complete co-noetherian Lattice holds MIRRS L is infimum-dense

proof end;

registration

let L be complete co-noetherian Lattice;
cluster MIRRS L -> infimum-dense ;
coherence by Lm10;

end;

Lm11: for L being complete noetherian Lattice holds JIRRS L is supremum-dense

proof end;

registration

let L be complete noetherian Lattice;
cluster JIRRS L -> supremum-dense ;
coherence by Lm11;

end;