LATTICES: Introduction to Lattice Theory

:: Introduction to Lattice Theory
:: by Stanis{\l}aw \.Zukowski
::
:: Received April 14, 1989
:: Copyright (c) 1990-2016 Association of Mizar Users

environ

vocabularies HIDDEN, STRUCT_0, BINOP_1, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, FUNCT_1, PBOOLE, XXREAL_2, CAT_1, LATTICES, CARD_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, CARD_1, STRUCT_0, BINOP_1;
definitions ;
theorems ZFMISC_1, SUBSET_1;
schemes ;
registrations XBOOLE_0, SUBSET_1, CARD_1, STRUCT_0;
constructors HIDDEN, BINOP_1, STRUCT_0;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS;
equalities STRUCT_0;
expansions STRUCT_0;

definition

attr c₁ is strict ;
struct /\-SemiLattStr -> 1-sorted ;
aggr /\-SemiLattStr(# carrier, L_meet #) -> /\-SemiLattStr ;
sel L_meet c₁ -> BinOp of the carrier of c₁;

end;

definition

attr c₁ is strict ;
struct \/-SemiLattStr -> 1-sorted ;
aggr \/-SemiLattStr(# carrier, L_join #) -> \/-SemiLattStr ;
sel L_join c₁ -> BinOp of the carrier of c₁;

end;

definition

attr c₁ is strict ;
struct LattStr -> /\-SemiLattStr , \/-SemiLattStr ;
aggr LattStr(# carrier, L_join, L_meet #) -> LattStr ;

end;

registration

let D be non empty set ;
let u be BinOp of D;

cluster \/-SemiLattStr(# D,u #) -> non empty ;

cluster /\-SemiLattStr(# D,u #) -> non empty ;

end;

registration

let D be non empty set ;
let u, n be BinOp of D;

cluster LattStr(# D,u,n #) -> non empty ;

end;

registration

cluster 1 -element strict for \/-SemiLattStr ;

proof end;

cluster 1 -element strict for /\-SemiLattStr ;

proof end;

cluster 1 -element strict for LattStr ;

proof end;

end;

definition

let G be non empty \/-SemiLattStr ;
let p, q be Element of G;

func p "\/" q -> Element of G equals :: LATTICES:def 1
the L_join of G . (p,q);

end;

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

definition

let G be non empty /\-SemiLattStr ;
let p, q be Element of G;

func p "/\" q -> Element of G equals :: LATTICES:def 2
the L_meet of G . (p,q);

end;

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

definition

let G be non empty \/-SemiLattStr ;
let p, q be Element of G;

pred p [= q means :Def3: :: LATTICES:def 3
p "\/" q = q;

end;

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

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 ;

attr IT is join-commutative means :Def4: :: LATTICES:def 4
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;

end;

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

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

definition

let IT be non empty /\-SemiLattStr ;

attr IT is meet-commutative means :Def6: :: LATTICES:def 6
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;

end;

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

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

definition

let IT be non empty LattStr ;

attr IT is meet-absorbing means :Def8: :: LATTICES:def 8
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;

end;

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

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

definition

let IT be non empty LattStr ;

attr IT is Lattice-like means :: 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 );

end;

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

registration

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

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

end;

registration

cluster non empty strict join-commutative join-associative for \/-SemiLattStr ;

proof end;

cluster non empty strict meet-commutative meet-associative for /\-SemiLattStr ;

proof end;

cluster non empty strict Lattice-like for LattStr ;

proof end;

end;

definition

mode Lattice is non empty Lattice-like LattStr ;

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 by Def4;

end;

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 by Def6;

end;

definition

let IT be non empty LattStr ;

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

end;

:: deftheorem Def11 defines distributive LATTICES:def 11 :

definition

let IT be non empty LattStr ;

attr IT is modular means :: LATTICES:def 12
for a, b, c being Element of IT st a [= c holds
a "\/" (b "/\" c) = (a "\/" b) "/\" c;

end;

:: deftheorem defines modular LATTICES:def 12 :

definition

let IT be non empty /\-SemiLattStr ;

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

end;

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

definition

let IT be non empty \/-SemiLattStr ;

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

end;

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

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

proof end;

registration

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 ;

proof end;

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;

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;

definition

let IT be non empty LattStr ;

attr IT is bounded means :: LATTICES:def 15
( IT is lower-bounded & IT is upper-bounded );

end;

:: deftheorem defines bounded LATTICES:def 15 :

registration

cluster non empty lower-bounded upper-bounded -> non empty bounded for LattStr ;

cluster non empty bounded -> non empty lower-bounded upper-bounded for LattStr ;

end;

registration

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

proof end;

end;

definition

mode 01_Lattice is bounded Lattice;

end;

definition

let L be non empty /\-SemiLattStr ;
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 by A1;
uniqueness

proof end;

end;

:: deftheorem Def16 defines Bottom LATTICES:def 16 :

definition

let L be non empty \/-SemiLattStr ;
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 by A1;
uniqueness

proof end;

end;

:: deftheorem Def17 defines Top LATTICES:def 17 :

definition

let L be non empty LattStr ;
let a, b be Element of L;

pred a is_a_complement_of b means :: LATTICES:def 18
( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L );

end;

:: deftheorem defines is_a_complement_of LATTICES:def 18 :

definition

let IT be non empty LattStr ;

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;

end;

:: deftheorem Def19 defines complemented LATTICES:def 19 :

registration

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

proof end;

end;

definition

mode C_Lattice is complemented 01_Lattice;

end;

definition

let IT be non empty LattStr ;

attr IT is Boolean means :: LATTICES:def 20
( IT is bounded & IT is complemented & IT is distributive );

end;

:: deftheorem defines Boolean LATTICES:def 20 :

registration

cluster non empty Boolean -> non empty distributive bounded complemented for LattStr ;

cluster non empty distributive bounded complemented -> non empty Boolean for LattStr ;

end;

registration

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

proof end;

end;

definition

mode B_Lattice is Boolean Lattice;

end;

registration

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

reduce a "\/" a to a;

proof end;

end;

registration

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

reduce a "/\" a to a;

proof end;

end;

theorem :: LATTICES:1

canceled;

theorem :: LATTICES:2

canceled;

::$CT 2

theorem Th1: :: 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) )

proof end;

theorem Th2: :: 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 ) by Def8, Def9;

theorem Th3: :: 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

proof end;

theorem Th4: :: LATTICES:6

for L being non empty meet-commutative meet-absorbing LattStr
for a, b being Element of L holds a "/\" b [= a by Def8;

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 ;

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 by Def5;

theorem Th6: :: 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

proof end;

theorem Th7: :: 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

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

proof end;

theorem Th9: :: LATTICES:11

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

proof end;

theorem Th10: :: LATTICES:12

for L being D_Lattice
for a, b, c 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)

proof end;

registration

cluster non empty Lattice-like distributive -> modular for LattStr ;

proof end;

end;

registration

let L be 0_Lattice;
let a be Element of L;

reduce (Bottom L) "\/" a to a;

proof end;

reduce (Bottom L) "/\" a to Bottom L;

reducibility by Def16;

end;

theorem :: LATTICES:14

for L being 0_Lattice
for a being Element of L holds (Bottom L) "\/" a = a ;

theorem :: LATTICES:15

for L being 0_Lattice
for a being Element of L holds (Bottom L) "/\" a = Bottom L ;

theorem :: LATTICES:16

for L being 0_Lattice
for a being Element of L holds Bottom L [= a ;

registration

let L be 1_Lattice;
let a be Element of L;

reduce (Top L) "/\" a to a;

proof end;

reduce (Top L) "\/" a to Top L;

reducibility by Def17;

end;

theorem :: LATTICES:17

for L being 1_Lattice
for a being Element of L holds (Top L) "/\" a = a ;

theorem :: LATTICES:18

for L being 1_Lattice
for a being Element of L holds (Top L) "\/" a = Top L ;

theorem :: LATTICES:19

for L being 1_Lattice
for a being Element of L holds a [= Top L

proof end;

definition

let L be non empty LattStr ;
let x be Element of L;
assume A1: L is complemented D_Lattice ;

func x ` -> Element of L means :Def21: :: LATTICES:def 21
it is_a_complement_of x;

existence by A1, Def19;
uniqueness by A1, Th10;

end;

:: deftheorem Def21 defines ` LATTICES:def 21 :

theorem Th18: :: LATTICES:20

for L being B_Lattice
for a being Element of L holds (a `) "/\" a = Bottom L

proof end;

theorem Th19: :: LATTICES:21

for L being B_Lattice
for a being Element of L holds (a `) "\/" a = Top L

proof end;

registration

let L be B_Lattice;
let a be Element of L;

reduce (a `) ` to a;

proof end;

end;

theorem :: LATTICES:22

for L being B_Lattice
for a being Element of L holds (a `) ` = a ;

theorem Th21: :: LATTICES:23

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

proof end;

theorem :: LATTICES:24

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

proof end;

theorem Th23: :: LATTICES:25

for L being B_Lattice
for a, b being Element of L holds
( b "/\" a = Bottom L iff b [= a ` )

proof end;

theorem :: LATTICES:26

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

proof end;

:: missing, 2009.07.28, A.T.

definition

let L be Lattice;
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;

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;

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;

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;

end;

:: deftheorem Def22 defines initial LATTICES:def 22 :

:: deftheorem Def23 defines final LATTICES:def 23 :

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

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

registration

let L be Lattice;

cluster [#] L -> non empty initial final ;

end;

registration

let L be Lattice;

cluster non empty initial final for M3( bool the carrier of L);

proof end;

cluster empty -> initial final for M3( bool the carrier of L);

cluster initial -> meet-closed for M3( bool the carrier of L);

coherence by Th4;

cluster final -> join-closed for M3( bool the carrier of L);

coherence by Th3;

end;

theorem :: LATTICES:27

for L being Lattice
for S being non empty initial final Subset of L holds S = [#] L

proof end;