:: by Christoph Schwarzweller

::

:: Received June 9, 1999

:: Copyright (c) 1999-2018 Association of Mizar Users

registration

ex b_{1} being Lattice st b_{1} is finite
end;

cluster non empty finite join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for Lattice;

existence ex b

proof 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
end;

definition

let L be Lattice;

let D be Subset of L;

{ (d %) where d is Element of L : d in D } is Subset of (LattPOSet L)

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

{ (d %) where d is Element of L : d in D } is Subset of (LattPOSet L)

proof 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 } ;

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

{ (% d) where d is Element of (LattPOSet L) : d in D } is Subset of L

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

{ (% d) where d is Element of (LattPOSet L) : d in D } is Subset of L

proof 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 } ;

for L being Lattice

for D being Subset of (LattPOSet L) holds % D = { (% d) where d is Element of (LattPOSet L) : d in D } ;

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

proof end;

:: deftheorem Def3 defines noetherian LATTICE6:def 3 :

for L being Lattice holds

( L is noetherian iff LattPOSet L is well_founded );

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

for L being Lattice holds

( L is co-noetherian iff (LattPOSet L) ~ is well_founded );

registration

ex b_{1} being Lattice st

( b_{1} is noetherian & b_{1} is upper-bounded & b_{1} is lower-bounded & b_{1} is complete )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded complete noetherian for Lattice;

existence ex b

( b

proof end;

registration

ex b_{1} being Lattice st

( b_{1} is co-noetherian & b_{1} is upper-bounded & b_{1} is lower-bounded & b_{1} is complete )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded complete co-noetherian for Lattice;

existence ex b

( b

proof end;

Lm7: for L being finite Lattice holds

( L is noetherian & L is co-noetherian )

by Lm6;

registration

coherence

for b_{1} being Lattice st b_{1} is finite holds

b_{1} is noetherian
;

coherence

for b_{1} being Lattice st b_{1} is finite holds

b_{1} is co-noetherian
by Lm7;

end;
for b

b

coherence

for b

b

definition

let L be Lattice;

let a, b be Element of L;

end;
let a, b be Element of L;

pred a is-upper-neighbour-of b means :: LATTICE6:def 5

( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds

c = b ) );

( a <> b & b [= a & ( for c being Element of L st b [= c & c [= a & not c = a holds

c = b ) );

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

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;
let a, b be Element of L;

synonym b is-lower-neighbour-of a for a is-upper-neighbour-of b;

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

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 )

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 )

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

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

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 )

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;

coherence

"/\" ( { d where d is Element of L : ( a [= d & d <> a ) } ,L) is Element of L;

;

coherence

"\/" ( { d where d is Element of L : ( d [= a & d <> a ) } ,L) is Element of L;

;

end;
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 "/\" ( { d where d is Element of L : ( a [= d & d <> a ) } ,L);

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 "\/" ( { d where d is Element of L : ( d [= a & d <> a ) } ,L);

coherence

"\/" ( { d where d is Element of L : ( d [= a & d <> a ) } ,L) is Element of L;

;

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

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

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

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

for L being complete Lattice

for a being Element of L holds

( a is completely-meet-irreducible iff a *' <> a );

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

for L being complete Lattice

for a being Element of L holds

( a is completely-join-irreducible iff *' a <> a );

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 *' ) )

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

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

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

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

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 )

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

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 )

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;

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;

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

for L being Lattice

for a being Element of L holds

( a is atomic iff a is-upper-neighbour-of Bottom L );

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

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

for L being complete Lattice

for a being Element of L st a is atomic holds

a is completely-join-irreducible

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

for a being Element of L st a is co-atomic holds

a is completely-meet-irreducible

proof end;

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

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

ex b_{1} being Lattice st

( b_{1} is strict & b_{1} is 1 -element )
end;

cluster non empty 1 -element strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like for Lattice;

existence ex b

( b

proof end;

registration

ex b_{1} being Lattice st

( b_{1} is atomic & b_{1} is complete )
end;

cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like complete atomic for Lattice;

existence ex b

( b

proof end;

definition

let L be complete Lattice;

let D be Subset of L;

end;
let D be Subset of L;

attr D is supremum-dense means :: LATTICE6:def 13

for a being Element of L ex D9 being Subset of D st a = "\/" (D9,L);

for a being Element of L ex D9 being Subset of D st a = "\/" (D9,L);

attr D is infimum-dense means :: LATTICE6:def 14

for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L);

for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L);

:: deftheorem 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 D9 being Subset of D st a = "\/" (D9,L) );

for L being complete Lattice

for D being Subset of L holds

( D is supremum-dense iff for a being Element of L ex D9 being Subset of D st a = "\/" (D9,L) );

:: deftheorem 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 D9 being Subset of D st a = "/\" (D9,L) );

for L being complete Lattice

for D being Subset of L holds

( D is infimum-dense iff for a being Element of L ex D9 being Subset of D st a = "/\" (D9,L) );

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

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

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 )

for D being Subset of L holds

( D is infimum-dense iff D % is order-generating )

proof end;

definition

let L be complete Lattice;

coherence

{ a where a is Element of L : a is completely-meet-irreducible } is Subset of L;

coherence

{ a where a is Element of L : a is completely-join-irreducible } is Subset of L;

end;
func MIRRS L -> Subset of L equals :: LATTICE6:def 15

{ a where a is Element of L : a is completely-meet-irreducible } ;

correctness { a where a is Element of L : a is completely-meet-irreducible } ;

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 { a where a is Element of L : a is completely-join-irreducible } ;

coherence

{ a where a is Element of L : a is completely-join-irreducible } is Subset of L;

proof 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 } ;

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

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

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

proof end;

registration
end;

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

proof end;

registration
end;