:: LATTICE6 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
cluster finite LattStr ;
existence
ex b1 being Lattice st b1 is finite
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
for b1 being Lattice st b1 is finite holds
b1 is complete
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
{ (d % ) where d is Element of L : d in D } is Subset of (LattPOSet L)
proof end;
end;

:: deftheorem defines % LATTICE6:def 1 :
for L being Lattice
for D being Subset of L holds D % = { (d % ) where d is Element of L : d in D } ;

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
{ (% d) where d is Element of (LattPOSet L) : d in D } is Subset of L
proof end;
end;

:: deftheorem defines % LATTICE6:def 2 :
for L being Lattice
for D being Subset of (LattPOSet L) holds % D = { (% d) where d is Element of (LattPOSet L) : d in D } ;

registration
let L be finite Lattice;
cluster LattPOSet L -> well_founded ;
coherence
LattPOSet L is well_founded
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 :
for L being Lattice holds
( L is noetherian iff LattPOSet L is well_founded );

:: deftheorem Def4 defines co-noetherian LATTICE6:def 4 :
for L being Lattice holds
( L is co-noetherian iff (LattPOSet L) ~ is well_founded );

registration
cluster lower-bounded upper-bounded complete noetherian LattStr ;
existence
ex b1 being Lattice st
( b1 is noetherian & b1 is upper-bounded & b1 is lower-bounded & b1 is complete )
proof end;
end;

registration
cluster lower-bounded upper-bounded complete co-noetherian LattStr ;
existence
ex b1 being Lattice st
( b1 is co-noetherian & b1 is upper-bounded & b1 is lower-bounded & b1 is complete )
proof end;
end;

theorem :: LATTICE6:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
for b1 being Lattice st b1 is finite holds
b1 is noetherian
by Lm7;
cluster finite -> co-noetherian LattStr ;
coherence
for b1 being Lattice st b1 is finite holds
b1 is co-noetherian
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 :
for L being Lattice
for a, b being Element of L holds
( a is-upper-neighbour-of b iff ( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds
c = b ) ) );

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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
coherence
"/\" { d where d is Element of L : ( a [= d & d <> a ) } ,L is Element of L
;
;
func *' a -> Element of L equals :: LATTICE6:def 7
"\/" { d where d is Element of L : ( d [= a & d <> a ) } ,L;
correctness
coherence
"\/" { d where d is Element of L : ( d [= a & d <> a ) } ,L is Element of L
;
;
end;

:: deftheorem defines *' LATTICE6:def 6 :
for L being complete Lattice
for a being Element of L holds a *' = "/\" { d where d is Element of L : ( a [= d & d <> a ) } ,L;

:: deftheorem defines *' LATTICE6:def 7 :
for L being complete Lattice
for a being Element of L holds *' a = "\/" { d where d is Element of L : ( d [= a & d <> a ) } ,L;

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 :
for L being complete Lattice
for a being Element of L holds
( a is completely-meet-irreducible iff a *' <> a );

:: deftheorem Def9 defines completely-join-irreducible LATTICE6:def 9 :
for L being complete Lattice
for a being Element of L holds
( a is completely-join-irreducible iff *' a <> a );

theorem Th9: :: LATTICE6:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice
for a being Element of L holds
( a [= a *' & *' a [= a )
proof end;

theorem :: LATTICE6:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice holds
( (Top L) *' = Top L & (Top L) % is meet-irreducible )
proof end;

theorem :: LATTICE6:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for L being complete Lattice holds
( *' (Bottom L) = Bottom L & (Bottom L) % is join-irreducible )
proof end;

theorem Th12: :: LATTICE6:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for L being Lattice
for a being Element of L holds
( a is atomic iff a is-upper-neighbour-of Bottom L );

:: deftheorem Def11 defines co-atomic LATTICE6:def 11 :
for L being Lattice
for a being Element of L holds
( a is co-atomic iff a is-lower-neighbour-of Top L );

theorem :: LATTICE6:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 :
for L being Lattice holds
( L is atomic iff 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 ) );

registration
cluster strict trivial LattStr ;
existence
ex b1 being Lattice st
( b1 is strict & not b1 is empty & b1 is trivial )
proof end;
end;

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

registration
cluster complete atomic LattStr ;
existence
ex b1 being Lattice st
( b1 is atomic & b1 is complete )
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 :
for L being complete Lattice
for D being Subset of L holds
( D is supremum-dense iff for a being Element of L ex D' being Subset of D st a = "\/" D',L );

:: deftheorem Def14 defines infimum-dense LATTICE6:def 14 :
for L being complete Lattice
for D being Subset of L holds
( D is infimum-dense iff for a being Element of L ex D' being Subset of D st a = "/\" D',L );

theorem Th23: :: LATTICE6:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
coherence
{ a where a is Element of L : a is completely-meet-irreducible } is Subset of L
;
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
coherence
{ a where a is Element of L : a is completely-join-irreducible } is Subset of L
;
proof end;
end;

:: deftheorem defines MIRRS LATTICE6:def 15 :
for L being complete Lattice holds MIRRS L = { a where a is Element of L : a is completely-meet-irreducible } ;

:: deftheorem defines JIRRS LATTICE6:def 16 :
for L being complete Lattice holds JIRRS L = { a where a is Element of L : a is completely-join-irreducible } ;

theorem :: LATTICE6:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
MIRRS L is infimum-dense
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
JIRRS L is supremum-dense
by Lm11;
end;