:: by Stanis{\l}aw \.Zukowski

::

:: Received April 14, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

definition

attr c_{1} is strict ;

struct /\-SemiLattStr -> 1-sorted ;

aggr /\-SemiLattStr(# carrier, L_meet #) -> /\-SemiLattStr ;

sel L_meet c_{1} -> BinOp of the carrier of c_{1};

end;
struct /\-SemiLattStr -> 1-sorted ;

aggr /\-SemiLattStr(# carrier, L_meet #) -> /\-SemiLattStr ;

sel L_meet c

definition

attr c_{1} is strict ;

struct \/-SemiLattStr -> 1-sorted ;

aggr \/-SemiLattStr(# carrier, L_join #) -> \/-SemiLattStr ;

sel L_join c_{1} -> BinOp of the carrier of c_{1};

end;
struct \/-SemiLattStr -> 1-sorted ;

aggr \/-SemiLattStr(# carrier, L_join #) -> \/-SemiLattStr ;

sel L_join c

definition

attr c_{1} is strict ;

struct LattStr -> /\-SemiLattStr , \/-SemiLattStr ;

aggr LattStr(# carrier, L_join, L_meet #) -> LattStr ;

end;
struct LattStr -> /\-SemiLattStr , \/-SemiLattStr ;

aggr LattStr(# carrier, L_join, L_meet #) -> LattStr ;

registration

let D be non empty set ;

let u be BinOp of D;

coherence

not \/-SemiLattStr(# D,u #) is empty ;

coherence

not /\-SemiLattStr(# D,u #) is empty ;

end;
let u be BinOp of D;

coherence

not \/-SemiLattStr(# D,u #) is empty ;

coherence

not /\-SemiLattStr(# D,u #) is empty ;

registration
end;

registration

existence

ex b_{1} being \/-SemiLattStr st

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

ex b_{1} being /\-SemiLattStr st

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

ex b_{1} being LattStr st

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

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

existence ex b

( b

proof end;

definition

let G be non empty \/-SemiLattStr ;

let p, q be Element of G;

coherence

the L_join of G . (p,q) is Element of G ;

end;
let p, q be Element of G;

coherence

the L_join of G . (p,q) is Element of G ;

:: deftheorem defines "\/" LATTICES:def 1 :

for G being non empty \/-SemiLattStr

for p, q being Element of G holds p "\/" q = the L_join of G . (p,q);

for G being non empty \/-SemiLattStr

for p, q being Element of G holds p "\/" q = the L_join of G . (p,q);

definition

let G be non empty /\-SemiLattStr ;

let p, q be Element of G;

coherence

the L_meet of G . (p,q) is Element of G ;

end;
let p, q be Element of G;

coherence

the L_meet of G . (p,q) is Element of G ;

:: deftheorem defines "/\" LATTICES:def 2 :

for G being non empty /\-SemiLattStr

for p, q being Element of G holds p "/\" q = the L_meet of G . (p,q);

for G being non empty /\-SemiLattStr

for p, q being Element of G holds p "/\" q = the L_meet of G . (p,q);

:: deftheorem Def3 defines [= LATTICES:def 3 :

for G being non empty \/-SemiLattStr

for p, q being Element of G holds

( p [= q iff p "\/" q = q );

for G being non empty \/-SemiLattStr

for p, q being Element of G holds

( p [= q iff p "\/" q = q );

Lm1: for uu, nn being BinOp of (bool {})

for x, y being Element of LattStr(# (bool {}),uu,nn #) holds x = y

proof end;

Lm2: for n being BinOp of (bool {})

for x, y being Element of \/-SemiLattStr(# (bool {}),n #) holds x = y

proof end;

Lm3: for n being BinOp of (bool {})

for x, y being Element of /\-SemiLattStr(# (bool {}),n #) holds x = y

proof end;

definition

let IT be non empty \/-SemiLattStr ;

end;
attr IT is join-commutative means :Def4: :: LATTICES:def 4

for a, b being Element of IT holds a "\/" b = b "\/" a;

for a, b being Element of IT holds a "\/" b = b "\/" a;

attr IT is join-associative means :Def5: :: LATTICES:def 5

for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c;

for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c;

:: deftheorem Def4 defines join-commutative LATTICES:def 4 :

for IT being non empty \/-SemiLattStr holds

( IT is join-commutative iff for a, b being Element of IT holds a "\/" b = b "\/" a );

for IT being non empty \/-SemiLattStr holds

( IT is join-commutative iff for a, b being Element of IT holds a "\/" b = b "\/" a );

:: deftheorem Def5 defines join-associative LATTICES:def 5 :

for IT being non empty \/-SemiLattStr holds

( IT is join-associative iff for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c );

for IT being non empty \/-SemiLattStr holds

( IT is join-associative iff for a, b, c being Element of IT holds a "\/" (b "\/" c) = (a "\/" b) "\/" c );

definition

let IT be non empty /\-SemiLattStr ;

end;
attr IT is meet-commutative means :Def6: :: LATTICES:def 6

for a, b being Element of IT holds a "/\" b = b "/\" a;

for a, b being Element of IT holds a "/\" b = b "/\" a;

attr IT is meet-associative means :Def7: :: LATTICES:def 7

for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c;

for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c;

:: deftheorem Def6 defines meet-commutative LATTICES:def 6 :

for IT being non empty /\-SemiLattStr holds

( IT is meet-commutative iff for a, b being Element of IT holds a "/\" b = b "/\" a );

for IT being non empty /\-SemiLattStr holds

( IT is meet-commutative iff for a, b being Element of IT holds a "/\" b = b "/\" a );

:: deftheorem Def7 defines meet-associative LATTICES:def 7 :

for IT being non empty /\-SemiLattStr holds

( IT is meet-associative iff for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c );

for IT being non empty /\-SemiLattStr holds

( IT is meet-associative iff for a, b, c being Element of IT holds a "/\" (b "/\" c) = (a "/\" b) "/\" c );

definition

let IT be non empty LattStr ;

end;
attr IT is meet-absorbing means :Def8: :: LATTICES:def 8

for a, b being Element of IT holds (a "/\" b) "\/" b = b;

for a, b being Element of IT holds (a "/\" b) "\/" b = b;

attr IT is join-absorbing means :Def9: :: LATTICES:def 9

for a, b being Element of IT holds a "/\" (a "\/" b) = a;

for a, b being Element of IT holds a "/\" (a "\/" b) = a;

:: deftheorem Def8 defines meet-absorbing LATTICES:def 8 :

for IT being non empty LattStr holds

( IT is meet-absorbing iff for a, b being Element of IT holds (a "/\" b) "\/" b = b );

for IT being non empty LattStr holds

( IT is meet-absorbing iff for a, b being Element of IT holds (a "/\" b) "\/" b = b );

:: deftheorem Def9 defines join-absorbing LATTICES:def 9 :

for IT being non empty LattStr holds

( IT is join-absorbing iff for a, b being Element of IT holds a "/\" (a "\/" b) = a );

for IT being non empty LattStr holds

( IT is join-absorbing iff for a, b being Element of IT holds a "/\" (a "\/" b) = a );

definition

let IT be non empty LattStr ;

end;
attr IT is Lattice-like means :Def10: :: LATTICES:def 10

( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing );

( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing );

:: deftheorem Def10 defines Lattice-like LATTICES:def 10 :

for IT being non empty LattStr holds

( IT is Lattice-like iff ( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing ) );

for IT being non empty LattStr holds

( IT is Lattice-like iff ( IT is join-commutative & IT is join-associative & IT is meet-absorbing & IT is meet-commutative & IT is meet-associative & IT is join-absorbing ) );

registration

for b_{1} being non empty LattStr st b_{1} is Lattice-like holds

( b_{1} is join-commutative & b_{1} is join-associative & b_{1} is meet-absorbing & b_{1} is meet-commutative & b_{1} is meet-associative & b_{1} is join-absorbing )
by Def10;

for b_{1} being non empty LattStr st b_{1} is join-commutative & b_{1} is join-associative & b_{1} is meet-absorbing & b_{1} is meet-commutative & b_{1} is meet-associative & b_{1} is join-absorbing holds

b_{1} is Lattice-like
by Def10;

end;

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

coherence for b

( b

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

coherence for b

b

registration

existence

ex b_{1} being non empty \/-SemiLattStr st

( b_{1} is strict & b_{1} is join-commutative & b_{1} is join-associative )

ex b_{1} being non empty /\-SemiLattStr st

( b_{1} is strict & b_{1} is meet-commutative & b_{1} is meet-associative )

ex b_{1} being non empty LattStr st

( b_{1} is strict & b_{1} is Lattice-like )

end;
ex b

( b

proof end;

existence ex b

( b

proof end;

existence ex b

( b

proof end;

definition

let L be non empty join-commutative \/-SemiLattStr ;

let a, b be Element of L;

:: original: "\/"

redefine func a "\/" b -> Element of L;

commutativity

for a, b being Element of L holds a "\/" b = b "\/" a by Def4;

end;
let a, b be Element of L;

:: original: "\/"

redefine func a "\/" b -> Element of L;

commutativity

for a, b being Element of L holds a "\/" b = b "\/" a by Def4;

definition

let L be non empty meet-commutative /\-SemiLattStr ;

let a, b be Element of L;

:: original: "/\"

redefine func a "/\" b -> Element of L;

commutativity

for a, b being Element of L holds a "/\" b = b "/\" a by Def6;

end;
let a, b be Element of L;

:: original: "/\"

redefine func a "/\" b -> Element of L;

commutativity

for a, b being Element of L holds a "/\" b = b "/\" a by Def6;

definition

let IT be non empty LattStr ;

end;
attr IT is distributive means :Def11: :: LATTICES:def 11

for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c);

for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c);

:: deftheorem Def11 defines distributive LATTICES:def 11 :

for IT being non empty LattStr holds

( IT is distributive iff for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) );

for IT being non empty LattStr holds

( IT is distributive iff for a, b, c being Element of IT holds a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) );

:: deftheorem Def12 defines modular LATTICES:def 12 :

for IT being non empty LattStr holds

( IT is modular iff for a, b, c being Element of IT st a [= c holds

a "\/" (b "/\" c) = (a "\/" b) "/\" c );

for IT being non empty LattStr holds

( IT is modular iff for a, b, c being Element of IT st a [= c holds

a "\/" (b "/\" c) = (a "\/" b) "/\" c );

definition

let IT be non empty /\-SemiLattStr ;

end;
attr IT is lower-bounded means :Def13: :: LATTICES:def 13

ex c being Element of IT st

for a being Element of IT holds

( c "/\" a = c & a "/\" c = c );

ex c being Element of IT st

for a being Element of IT holds

( c "/\" a = c & a "/\" c = c );

:: deftheorem Def13 defines lower-bounded LATTICES:def 13 :

for IT being non empty /\-SemiLattStr holds

( IT is lower-bounded iff ex c being Element of IT st

for a being Element of IT holds

( c "/\" a = c & a "/\" c = c ) );

for IT being non empty /\-SemiLattStr holds

( IT is lower-bounded iff ex c being Element of IT st

for a being Element of IT holds

( c "/\" a = c & a "/\" c = c ) );

definition

let IT be non empty \/-SemiLattStr ;

end;
attr IT is upper-bounded means :Def14: :: LATTICES:def 14

ex c being Element of IT st

for a being Element of IT holds

( c "\/" a = c & a "\/" c = c );

ex c being Element of IT st

for a being Element of IT holds

( c "\/" a = c & a "\/" c = c );

:: deftheorem Def14 defines upper-bounded LATTICES:def 14 :

for IT being non empty \/-SemiLattStr holds

( IT is upper-bounded iff ex c being Element of IT st

for a being Element of IT holds

( c "\/" a = c & a "\/" c = c ) );

for IT being non empty \/-SemiLattStr holds

( IT is upper-bounded iff ex c being Element of IT st

for a being Element of IT holds

( c "\/" a = c & a "\/" c = c ) );

Lm4: for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is Lattice

proof end;

registration

ex b_{1} being Lattice st

( b_{1} is strict & b_{1} is distributive & b_{1} is lower-bounded & b_{1} is upper-bounded & b_{1} is modular )
end;

cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded for LattStr ;

existence ex b

( b

proof end;

definition

mode D_Lattice is distributive Lattice;

mode M_Lattice is modular Lattice;

mode 0_Lattice is lower-bounded Lattice;

mode 1_Lattice is upper-bounded Lattice;

end;
mode M_Lattice is modular Lattice;

mode 0_Lattice is lower-bounded Lattice;

mode 1_Lattice is upper-bounded Lattice;

Lm5: for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is 0_Lattice

proof end;

Lm6: for n, u being BinOp of (bool {}) holds LattStr(# (bool {}),n,u #) is 1_Lattice

proof end;

:: deftheorem Def15 defines bounded LATTICES:def 15 :

for IT being non empty LattStr holds

( IT is bounded iff ( IT is lower-bounded & IT is upper-bounded ) );

for IT being non empty LattStr holds

( IT is bounded iff ( IT is lower-bounded & IT is upper-bounded ) );

registration

coherence

for b_{1} being non empty LattStr st b_{1} is lower-bounded & b_{1} is upper-bounded holds

b_{1} is bounded
by Def15;

coherence

for b_{1} being non empty LattStr st b_{1} is bounded holds

( b_{1} is lower-bounded & b_{1} is upper-bounded )
by Def15;

end;
for b

b

coherence

for b

( b

registration

ex b_{1} being Lattice st

( b_{1} is bounded & b_{1} is strict )
end;

cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded for LattStr ;

existence ex b

( b

proof end;

definition

let L be non empty /\-SemiLattStr ;

assume A1: L is lower-bounded ;

ex b_{1} being Element of L st

for a being Element of L holds

( b_{1} "/\" a = b_{1} & a "/\" b_{1} = b_{1} )
by A1, Def13;

uniqueness

for b_{1}, b_{2} being Element of L st ( for a being Element of L holds

( b_{1} "/\" a = b_{1} & a "/\" b_{1} = b_{1} ) ) & ( for a being Element of L holds

( b_{2} "/\" a = b_{2} & a "/\" b_{2} = b_{2} ) ) holds

b_{1} = b_{2}

end;
assume A1: L is lower-bounded ;

func Bottom L -> Element of L means :Def16: :: LATTICES:def 16

for a being Element of L holds

( it "/\" a = it & a "/\" it = it );

existence for a being Element of L holds

( it "/\" a = it & a "/\" it = it );

ex b

for a being Element of L holds

( b

uniqueness

for b

( b

( b

b

proof end;

:: deftheorem Def16 defines Bottom LATTICES:def 16 :

for L being non empty /\-SemiLattStr st L is lower-bounded holds

for b_{2} being Element of L holds

( b_{2} = Bottom L iff for a being Element of L holds

( b_{2} "/\" a = b_{2} & a "/\" b_{2} = b_{2} ) );

for L being non empty /\-SemiLattStr st L is lower-bounded holds

for b

( b

( b

definition

let L be non empty \/-SemiLattStr ;

assume A1: L is upper-bounded ;

ex b_{1} being Element of L st

for a being Element of L holds

( b_{1} "\/" a = b_{1} & a "\/" b_{1} = b_{1} )
by A1, Def14;

uniqueness

for b_{1}, b_{2} being Element of L st ( for a being Element of L holds

( b_{1} "\/" a = b_{1} & a "\/" b_{1} = b_{1} ) ) & ( for a being Element of L holds

( b_{2} "\/" a = b_{2} & a "\/" b_{2} = b_{2} ) ) holds

b_{1} = b_{2}

end;
assume A1: L is upper-bounded ;

func Top L -> Element of L means :Def17: :: LATTICES:def 17

for a being Element of L holds

( it "\/" a = it & a "\/" it = it );

existence for a being Element of L holds

( it "\/" a = it & a "\/" it = it );

ex b

for a being Element of L holds

( b

uniqueness

for b

( b

( b

b

proof end;

:: deftheorem Def17 defines Top LATTICES:def 17 :

for L being non empty \/-SemiLattStr st L is upper-bounded holds

for b_{2} being Element of L holds

( b_{2} = Top L iff for a being Element of L holds

( b_{2} "\/" a = b_{2} & a "\/" b_{2} = b_{2} ) );

for L being non empty \/-SemiLattStr st L is upper-bounded holds

for b

( b

( b

:: deftheorem Def18 defines is_a_complement_of LATTICES:def 18 :

for L being non empty LattStr

for a, b being Element of L holds

( a is_a_complement_of b iff ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) );

for L being non empty LattStr

for a, b being Element of L holds

( a is_a_complement_of b iff ( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) );

definition

let IT be non empty LattStr ;

end;
attr IT is complemented means :Def19: :: LATTICES:def 19

for b being Element of IT ex a being Element of IT st a is_a_complement_of b;

for b being Element of IT ex a being Element of IT st a is_a_complement_of b;

:: deftheorem Def19 defines complemented LATTICES:def 19 :

for IT being non empty LattStr holds

( IT is complemented iff for b being Element of IT ex a being Element of IT st a is_a_complement_of b );

for IT being non empty LattStr holds

( IT is complemented iff for b being Element of IT ex a being Element of IT st a is_a_complement_of b );

registration

ex b_{1} being Lattice st

( b_{1} is bounded & b_{1} is complemented & b_{1} is strict )
end;

cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like bounded complemented for LattStr ;

existence ex b

( b

proof end;

definition

let IT be non empty LattStr ;

end;
attr IT is Boolean means :Def20: :: LATTICES:def 20

( IT is bounded & IT is complemented & IT is distributive );

( IT is bounded & IT is complemented & IT is distributive );

:: deftheorem Def20 defines Boolean LATTICES:def 20 :

for IT being non empty LattStr holds

( IT is Boolean iff ( IT is bounded & IT is complemented & IT is distributive ) );

for IT being non empty LattStr holds

( IT is Boolean iff ( IT is bounded & IT is complemented & IT is distributive ) );

registration

coherence

for b_{1} being non empty LattStr st b_{1} is Boolean holds

( b_{1} is bounded & b_{1} is complemented & b_{1} is distributive )
by Def20;

coherence

for b_{1} being non empty LattStr st b_{1} is bounded & b_{1} is complemented & b_{1} is distributive holds

b_{1} is Boolean
by Def20;

end;
for b

( b

coherence

for b

b

registration

ex b_{1} being Lattice st

( b_{1} is Boolean & b_{1} is strict )
end;

cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Boolean for LattStr ;

existence ex b

( b

proof end;

registration

let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ;

let a be Element of L;

reducibility

a "\/" a = a

end;
let a be Element of L;

reducibility

a "\/" a = a

proof end;

registration

let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ;

let a be Element of L;

reducibility

a "/\" a = a

end;
let a be Element of L;

reducibility

a "/\" a = a

proof end;

theorem Th3: :: LATTICES:3

for L being Lattice holds

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

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

proof end;

theorem Th4: :: LATTICES:4

for L being non empty meet-absorbing join-absorbing LattStr

for a, b being Element of L holds

( a [= b iff a "/\" b = a )

for a, b being Element of L holds

( a [= b iff a "/\" b = a )

proof end;

theorem Th5: :: LATTICES:5

for L being non empty join-associative meet-commutative meet-absorbing join-absorbing LattStr

for a, b being Element of L holds a [= a "\/" b

for a, b being Element of L holds a [= a "\/" b

proof end;

theorem Th6: :: LATTICES:6

for L being non empty meet-commutative meet-absorbing LattStr

for a, b being Element of L holds a "/\" b [= a

for a, b being Element of L holds a "/\" b [= a

proof end;

definition

let L be non empty meet-commutative meet-absorbing join-absorbing LattStr ;

let a, b be Element of L;

:: original: [=

redefine pred a [= b;

reflexivity

for a being Element of L holds (L,b_{1},b_{1})

end;
let a, b be Element of L;

:: original: [=

redefine pred a [= b;

reflexivity

for a being Element of L holds (L,b

proof end;

theorem :: LATTICES:7

for L being non empty join-associative \/-SemiLattStr

for a, b, c being Element of L st a [= b & b [= c holds

a [= c

for a, b, c being Element of L st a [= b & b [= c holds

a [= c

proof end;

theorem Th8: :: LATTICES:8

for L being non empty join-commutative \/-SemiLattStr

for a, b being Element of L st a [= b & b [= a holds

a = b

for a, b being Element of L st a [= b & b [= a holds

a = b

proof end;

theorem Th9: :: LATTICES:9

for L being non empty meet-associative meet-absorbing join-absorbing LattStr

for a, b, c being Element of L st a [= b holds

a "/\" c [= b "/\" c

for a, b, c being Element of L st a [= b holds

a "/\" c [= b "/\" c

proof end;

theorem :: LATTICES:10

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

L is distributive

L is distributive

proof end;

theorem Th11: :: LATTICES:11

for L being D_Lattice

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

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

proof end;

theorem Th12: :: LATTICES:12

for L being D_Lattice

for c, a, b being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds

a = b

for c, a, b being Element of L st c "/\" a = c "/\" b & c "\/" a = c "\/" b holds

a = b

proof end;

theorem :: LATTICES:13

for L being D_Lattice

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

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

proof end;

registration
end;

registration

let L be 0_Lattice;

let a be Element of L;

reducibility

(Bottom L) "\/" a = a

(Bottom L) "/\" a = Bottom L by Def16;

end;
let a be Element of L;

reducibility

(Bottom L) "\/" a = a

proof end;

reducibility (Bottom L) "/\" a = Bottom L by Def16;

theorem :: LATTICES:15

registration

let L be 1_Lattice;

let a be Element of L;

reducibility

(Top L) "/\" a = a

(Top L) "\/" a = Top L by Def17;

end;
let a be Element of L;

reducibility

(Top L) "/\" a = a

proof end;

reducibility (Top L) "\/" a = Top L by Def17;

theorem :: LATTICES:18

definition

let L be non empty LattStr ;

let x be Element of L;

assume A1: L is complemented D_Lattice ;

existence

ex b_{1} being Element of L st b_{1} is_a_complement_of x
by A1, Def19;

uniqueness

for b_{1}, b_{2} being Element of L st b_{1} is_a_complement_of x & b_{2} is_a_complement_of x holds

b_{1} = b_{2}

end;
let x be Element of L;

assume A1: L is complemented D_Lattice ;

existence

ex b

uniqueness

for b

b

proof end;

:: deftheorem Def21 defines ` LATTICES:def 21 :

for L being non empty LattStr

for x being Element of L st L is complemented D_Lattice holds

for b_{3} being Element of L holds

( b_{3} = x ` iff b_{3} is_a_complement_of x );

for L being non empty LattStr

for x being Element of L st L is complemented D_Lattice holds

for b

( b

registration
end;

begin

:: missing, 2009.07.28, A.T.

definition

let L be Lattice;

let S be Subset of L;

end;
let S be Subset of L;

attr S is initial means :Def22: :: LATTICES:def 22

for p, q being Element of L st p [= q & q in S holds

p in S;

for p, q being Element of L st p [= q & q in S holds

p in S;

attr S is final means :Def23: :: LATTICES:def 23

for p, q being Element of L st p [= q & p in S holds

q in S;

for p, q being Element of L st p [= q & p in S holds

q in S;

attr S is meet-closed means :: LATTICES:def 24

for p, q being Element of L st p in S & q in S holds

p "/\" q in S;

for p, q being Element of L st p in S & q in S holds

p "/\" q in S;

attr S is join-closed means :: LATTICES:def 25

for p, q being Element of L st p in S & q in S holds

p "\/" q in S;

for p, q being Element of L st p in S & q in S holds

p "\/" q in S;

:: deftheorem Def22 defines initial LATTICES:def 22 :

for L being Lattice

for S being Subset of L holds

( S is initial iff for p, q being Element of L st p [= q & q in S holds

p in S );

for L being Lattice

for S being Subset of L holds

( S is initial iff for p, q being Element of L st p [= q & q in S holds

p in S );

:: deftheorem Def23 defines final LATTICES:def 23 :

for L being Lattice

for S being Subset of L holds

( S is final iff for p, q being Element of L st p [= q & p in S holds

q in S );

for L being Lattice

for S being Subset of L holds

( S is final iff for p, q being Element of L st p [= q & p in S holds

q in S );

:: deftheorem defines meet-closed LATTICES:def 24 :

for L being Lattice

for S being Subset of L holds

( S is meet-closed iff for p, q being Element of L st p in S & q in S holds

p "/\" q in S );

for L being Lattice

for S being Subset of L holds

( S is meet-closed iff for p, q being Element of L st p in S & q in S holds

p "/\" q in S );

:: deftheorem defines join-closed LATTICES:def 25 :

for L being Lattice

for S being Subset of L holds

( S is join-closed iff for p, q being Element of L st p in S & q in S holds

p "\/" q in S );

for L being Lattice

for S being Subset of L holds

( S is join-closed iff for p, q being Element of L st p in S & q in S holds

p "\/" q in S );

registration
end;

registration

let L be Lattice;

existence

ex b_{1} being Subset of L st

( b_{1} is initial & b_{1} is final & not b_{1} is empty )

for b_{1} being Subset of L st b_{1} is empty holds

( b_{1} is initial & b_{1} is final )

for b_{1} being Subset of L st b_{1} is initial holds

b_{1} is meet-closed

for b_{1} being Subset of L st b_{1} is final holds

b_{1} is join-closed

end;
existence

ex b

( b

proof end;

coherence for b

( b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;