:: LATTICES semantic presentation

definition

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

end;

definition

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

end;

definition

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

end;

registration

let c₁ be non empty set ;
let c₂ be BinOp of c₁;
cluster \/-SemiLattStr(# a₁,a₂ #) -> non empty ;
coherence by STRUCT_0:def 1;
cluster /\-SemiLattStr(# a₁,a₂ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

let c₁ be non empty set ;
let c₂, c₃ be BinOp of c₁;
cluster LattStr(# a₁,a₂,a₃ #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

cluster non empty strict \/-SemiLattStr ;
existence

proof end;

cluster non empty strict /\-SemiLattStr ;
existence

proof end;

cluster non empty strict LattStr ;
existence

proof end;

end;

definition

let c₁ be non empty \/-SemiLattStr ;
let c₂, c₃ be Element of c₁;
func c₂ "\/" c₃ -> Element of a₁ equals :: LATTICES:def 1
the L_join of a₁ . a₂,a₃;
coherence ;

end;

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

definition

let c₁ be non empty /\-SemiLattStr ;
let c₂, c₃ be Element of c₁;
func c₂ "/\" c₃ -> Element of a₁ equals :: LATTICES:def 2
the L_meet of a₁ . a₂,a₃;
coherence ;

end;

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

definition

let c₁ be non empty \/-SemiLattStr ;
let c₂, c₃ be Element of c₁;
pred c₂ [= c₃ means :Def3: :: LATTICES:def 3
a₂ "\/" a₃ = a₃;

end;

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

Lemma2: for b₁, b₂ being BinOp of bool {}
for b₃, b₄ being Element of LattStr(# (bool {} ),b₁,b₂ #) holds b₃ = b₄

proof end;

Lemma3: for b₁ being BinOp of bool {}
for b₂, b₃ being Element of \/-SemiLattStr(# (bool {} ),b₁ #) holds b₂ = b₃

proof end;

Lemma4: for b₁ being BinOp of bool {}
for b₂, b₃ being Element of /\-SemiLattStr(# (bool {} ),b₁ #) holds b₂ = b₃

proof end;

definition

let c₁ be non empty \/-SemiLattStr ;
attr a₁ is join-commutative means :Def4: :: LATTICES:def 4
for b₁, b₂ being Element of a₁ holds b₁ "\/" b₂ = b₂ "\/" b₁;
attr a₁ is join-associative means :Def5: :: LATTICES:def 5
for b₁, b₂, b₃ being Element of a₁ holds b₁ "\/" (b₂ "\/" b₃) = (b₁ "\/" b₂) "\/" b₃;

end;

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

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

definition

let c₁ be non empty /\-SemiLattStr ;
attr a₁ is meet-commutative means :Def6: :: LATTICES:def 6
for b₁, b₂ being Element of a₁ holds b₁ "/\" b₂ = b₂ "/\" b₁;
attr a₁ is meet-associative means :Def7: :: LATTICES:def 7
for b₁, b₂, b₃ being Element of a₁ holds b₁ "/\" (b₂ "/\" b₃) = (b₁ "/\" b₂) "/\" b₃;

end;

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

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

definition

let c₁ be non empty LattStr ;
attr a₁ is meet-absorbing means :Def8: :: LATTICES:def 8
for b₁, b₂ being Element of a₁ holds (b₁ "/\" b₂) "\/" b₂ = b₂;
attr a₁ is join-absorbing means :Def9: :: LATTICES:def 9
for b₁, b₂ being Element of a₁ holds b₁ "/\" (b₁ "\/" b₂) = b₁;

end;

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

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

definition

let c₁ be non empty LattStr ;
attr a₁ is Lattice-like means :Def10: :: LATTICES:def 10
( a₁ is join-commutative & a₁ is join-associative & a₁ is meet-absorbing & a₁ is meet-commutative & a₁ is meet-associative & a₁ is join-absorbing );

end;

:: deftheorem Def10 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 LattStr ;
coherence by Def10;
cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing -> non empty Lattice-like LattStr ;
coherence by Def10;

end;

registration

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

proof end;

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

proof end;

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

proof end;

end;

definition

mode Lattice is non empty Lattice-like LattStr ;

end;

definition

let c₁ be non empty join-commutative \/-SemiLattStr ;
let c₂, c₃ be Element of c₁;
redefine func "\/" as c₂ "\/" c₃ -> Element of a₁;
commutativity by Def4;

end;

definition

let c₁ be non empty meet-commutative /\-SemiLattStr ;
let c₂, c₃ be Element of c₁;
redefine func "/\" as c₂ "/\" c₃ -> Element of a₁;
commutativity by Def6;

end;

definition

let c₁ be non empty LattStr ;
attr a₁ is distributive means :Def11: :: LATTICES:def 11
for b₁, b₂, b₃ being Element of a₁ holds b₁ "/\" (b₂ "\/" b₃) = (b₁ "/\" b₂) "\/" (b₁ "/\" b₃);

end;

:: deftheorem Def11 defines distributive LATTICES:def 11 :

definition

let c₁ be non empty LattStr ;
attr a₁ is modular means :Def12: :: LATTICES:def 12
for b₁, b₂, b₃ being Element of a₁ st b₁ [= b₃ holds
b₁ "\/" (b₂ "/\" b₃) = (b₁ "\/" b₂) "/\" b₃;

end;

:: deftheorem Def12 defines modular LATTICES:def 12 :

definition

let c₁ be non empty /\-SemiLattStr ;
attr a₁ is lower-bounded means :Def13: :: LATTICES:def 13
ex b₁ being Element of a₁ st
for b₂ being Element of a₁ holds
( b₁ "/\" b₂ = b₁ & b₂ "/\" b₁ = b₁ );

end;

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

definition

let c₁ be non empty \/-SemiLattStr ;
attr a₁ is upper-bounded means :Def14: :: LATTICES:def 14
ex b₁ being Element of a₁ st
for b₂ being Element of a₁ holds
( b₁ "\/" b₂ = b₁ & b₂ "\/" b₁ = b₁ );

end;

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

Lemma16: for b₁, b₂ being BinOp of bool {} holds LattStr(# (bool {} ),b₁,b₂ #) is Lattice

proof end;

registration

cluster strict distributive modular lower-bounded upper-bounded LattStr ;
existence

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;

Lemma17: for b₁, b₂ being BinOp of bool {} holds LattStr(# (bool {} ),b₁,b₂ #) is 0_Lattice

proof end;

Lemma18: for b₁, b₂ being BinOp of bool {} holds LattStr(# (bool {} ),b₁,b₂ #) is 1_Lattice

proof end;

definition

let c₁ be non empty LattStr ;
attr a₁ is bounded means :Def15: :: LATTICES:def 15
( a₁ is lower-bounded & a₁ is upper-bounded );

end;

:: deftheorem Def15 defines bounded LATTICES:def 15 :

registration

cluster non empty lower-bounded upper-bounded -> non empty bounded LattStr ;
coherence by Def15;
cluster non empty bounded -> non empty lower-bounded upper-bounded LattStr ;
coherence by Def15;

end;

registration

cluster strict lower-bounded upper-bounded bounded LattStr ;
existence

proof end;

end;

definition

mode 01_Lattice is bounded Lattice;

end;

definition

let c₁ be non empty /\-SemiLattStr ;
assume E20: c₁ is lower-bounded ;
func Bottom c₁ -> Element of a₁ means :Def16: :: LATTICES:def 16
for b₁ being Element of a₁ holds
( a₂ "/\" b₁ = a₂ & b₁ "/\" a₂ = a₂ );
existence by E20, Def13;
uniqueness

proof end;

end;

:: deftheorem Def16 defines Bottom LATTICES:def 16 :

definition

let c₁ be non empty \/-SemiLattStr ;
assume E21: c₁ is upper-bounded ;
func Top c₁ -> Element of a₁ means :Def17: :: LATTICES:def 17
for b₁ being Element of a₁ holds
( a₂ "\/" b₁ = a₂ & b₁ "\/" a₂ = a₂ );
existence by E21, Def14;
uniqueness

proof end;

end;

:: deftheorem Def17 defines Top LATTICES:def 17 :

definition

let c₁ be non empty LattStr ;
let c₂, c₃ be Element of c₁;
pred c₂ is_a_complement_of c₃ means :Def18: :: LATTICES:def 18
( a₂ "\/" a₃ = Top a₁ & a₃ "\/" a₂ = Top a₁ & a₂ "/\" a₃ = Bottom a₁ & a₃ "/\" a₂ = Bottom a₁ );

end;

:: deftheorem Def18 defines is_a_complement_of LATTICES:def 18 :

definition

let c₁ be non empty LattStr ;
attr a₁ is complemented means :Def19: :: LATTICES:def 19
for b₁ being Element of a₁ ex b₂ being Element of a₁ st b₂ is_a_complement_of b₁;

end;

:: deftheorem Def19 defines complemented LATTICES:def 19 :

registration

cluster strict lower-bounded upper-bounded bounded complemented LattStr ;
existence

proof end;

end;

definition

mode C_Lattice is complemented 01_Lattice;

end;

definition

let c₁ be non empty LattStr ;
attr a₁ is Boolean means :Def20: :: LATTICES:def 20
( a₁ is bounded & a₁ is complemented & a₁ is distributive );

end;

:: deftheorem Def20 defines Boolean LATTICES:def 20 :

registration

cluster non empty Boolean -> non empty distributive lower-bounded upper-bounded bounded complemented LattStr ;
coherence by Def20;
cluster non empty distributive bounded complemented -> non empty Boolean LattStr ;
coherence by Def20;

end;

registration

cluster strict distributive lower-bounded upper-bounded bounded complemented Boolean LattStr ;
existence

proof end;

end;

definition

mode B_Lattice is Boolean Lattice;

end;

theorem Th1: :: LATTICES:1

canceled;

theorem Th2: :: LATTICES:2

canceled;

theorem Th3: :: LATTICES:3

canceled;

theorem Th4: :: LATTICES:4

canceled;

theorem Th5: :: LATTICES:5

canceled;

theorem Th6: :: LATTICES:6

canceled;

theorem Th7: :: LATTICES:7

canceled;

theorem Th8: :: LATTICES:8

canceled;

theorem Th9: :: LATTICES:9

canceled;

theorem Th10: :: LATTICES:10

canceled;

theorem Th11: :: LATTICES:11

canceled;

theorem Th12: :: LATTICES:12

canceled;

theorem Th13: :: LATTICES:13

canceled;

theorem Th14: :: LATTICES:14

canceled;

theorem Th15: :: LATTICES:15

canceled;

theorem Th16: :: LATTICES:16

canceled;

theorem Th17: :: LATTICES:17

for b₁ being non empty meet-commutative meet-absorbing join-absorbing LattStr
for b₂ being Element of b₁ holds b₂ "\/" b₂ = b₂

proof end;

theorem Th18: :: LATTICES:18

for b₁ being non empty meet-commutative meet-absorbing join-absorbing LattStr
for b₂ being Element of b₁ holds b₂ "/\" b₂ = b₂

proof end;

theorem Th19: :: LATTICES:19

for b₁ being Lattice holds
( ( for b₂, b₃, b₄ being Element of b₁ holds b₂ "/\" (b₃ "\/" b₄) = (b₂ "/\" b₃) "\/" (b₂ "/\" b₄) ) iff for b₂, b₃, b₄ being Element of b₁ holds b₂ "\/" (b₃ "/\" b₄) = (b₂ "\/" b₃) "/\" (b₂ "\/" b₄) )

proof end;

theorem Th20: :: LATTICES:20

canceled;

theorem Th21: :: LATTICES:21

for b₁ being non empty meet-absorbing join-absorbing LattStr
for b₂, b₃ being Element of b₁ holds
( b₂ [= b₃ iff b₂ "/\" b₃ = b₂ )

proof end;

theorem Th22: :: LATTICES:22

for b₁ being non empty join-associative meet-commutative meet-absorbing join-absorbing LattStr
for b₂, b₃ being Element of b₁ holds b₂ [= b₂ "\/" b₃

proof end;

theorem Th23: :: LATTICES:23

for b₁ being non empty meet-commutative meet-absorbing LattStr
for b₂, b₃ being Element of b₁ holds b₂ "/\" b₃ [= b₂

proof end;

definition

let c₁ be non empty meet-commutative meet-absorbing join-absorbing LattStr ;
let c₂, c₃ be Element of c₁;
redefine pred [= as c₂ [= c₃;
reflexivity

proof end;

end;

theorem Th24: :: LATTICES:24

canceled;

theorem Th25: :: LATTICES:25

for b₁ being non empty join-associative \/-SemiLattStr
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ & b₃ [= b₄ holds
b₂ [= b₄

proof end;

theorem Th26: :: LATTICES:26

for b₁ being non empty join-commutative \/-SemiLattStr
for b₂, b₃ being Element of b₁ st b₂ [= b₃ & b₃ [= b₂ holds
b₂ = b₃

proof end;

theorem Th27: :: LATTICES:27

for b₁ being non empty meet-associative meet-absorbing join-absorbing LattStr
for b₂, b₃, b₄ being Element of b₁ st b₂ [= b₃ holds
b₂ "/\" b₄ [= b₃ "/\" b₄

proof end;

theorem Th28: :: LATTICES:28

canceled;

theorem Th29: :: LATTICES:29

for b₁ being Lattice st ( for b₂, b₃, b₄ being Element of b₁ holds ((b₂ "/\" b₃) "\/" (b₃ "/\" b₄)) "\/" (b₄ "/\" b₂) = ((b₂ "\/" b₃) "/\" (b₃ "\/" b₄)) "/\" (b₄ "\/" b₂) ) holds
b₁ is distributive

proof end;

theorem Th30: :: LATTICES:30

canceled;

theorem Th31: :: LATTICES:31

for b₁ being D_Lattice
for b₂, b₃, b₄ being Element of b₁ holds b₂ "\/" (b₃ "/\" b₄) = (b₂ "\/" b₃) "/\" (b₂ "\/" b₄)

proof end;

theorem Th32: :: LATTICES:32

for b₁ being D_Lattice
for b₂, b₃, b₄ being Element of b₁ st b₂ "/\" b₃ = b₂ "/\" b₄ & b₂ "\/" b₃ = b₂ "\/" b₄ holds
b₃ = b₄

proof end;

theorem Th33: :: LATTICES:33

canceled;

theorem Th34: :: LATTICES:34

for b₁ being D_Lattice
for b₂, b₃, b₄ being Element of b₁ holds ((b₂ "\/" b₃) "/\" (b₃ "\/" b₄)) "/\" (b₄ "\/" b₂) = ((b₂ "/\" b₃) "\/" (b₃ "/\" b₄)) "\/" (b₄ "/\" b₂)

proof end;

registration

cluster distributive -> join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing modular LattStr ;
coherence

proof end;

end;

theorem Th35: :: LATTICES:35

canceled;

theorem Th36: :: LATTICES:36

canceled;

theorem Th37: :: LATTICES:37

canceled;

theorem Th38: :: LATTICES:38

canceled;

theorem Th39: :: LATTICES:39

for b₁ being 0_Lattice
for b₂ being Element of b₁ holds (Bottom b₁) "\/" b₂ = b₂

proof end;

theorem Th40: :: LATTICES:40

for b₁ being 0_Lattice
for b₂ being Element of b₁ holds (Bottom b₁) "/\" b₂ = Bottom b₁ by Def16;

theorem Th41: :: LATTICES:41

for b₁ being 0_Lattice
for b₂ being Element of b₁ holds Bottom b₁ [= b₂

proof end;

theorem Th42: :: LATTICES:42

canceled;

theorem Th43: :: LATTICES:43

for b₁ being 1_Lattice
for b₂ being Element of b₁ holds (Top b₁) "/\" b₂ = b₂

proof end;

theorem Th44: :: LATTICES:44

for b₁ being 1_Lattice
for b₂ being Element of b₁ holds (Top b₁) "\/" b₂ = Top b₁ by Def17;

theorem Th45: :: LATTICES:45

for b₁ being 1_Lattice
for b₂ being Element of b₁ holds b₂ [= Top b₁

proof end;

definition

let c₁ be non empty LattStr ;
let c₂ be Element of c₁;
assume E37: c₁ is complemented D_Lattice ;
func c₂ ` -> Element of a₁ means :Def21: :: LATTICES:def 21
a₃ is_a_complement_of a₂;
existence by E37, Def19;
uniqueness

proof end;

end;

:: deftheorem Def21 defines ` LATTICES:def 21 :

theorem Th46: :: LATTICES:46

canceled;

theorem Th47: :: LATTICES:47

for b₁ being B_Lattice
for b₂ being Element of b₁ holds (b₂ ` ) "/\" b₂ = Bottom b₁

proof end;

theorem Th48: :: LATTICES:48

for b₁ being B_Lattice
for b₂ being Element of b₁ holds (b₂ ` ) "\/" b₂ = Top b₁

proof end;

theorem Th49: :: LATTICES:49

for b₁ being B_Lattice
for b₂ being Element of b₁ holds (b₂ ` ) ` = b₂

proof end;

theorem Th50: :: LATTICES:50

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ "/\" b₃) ` = (b₂ ` ) "\/" (b₃ ` )

proof end;

theorem Th51: :: LATTICES:51

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds (b₂ "\/" b₃) ` = (b₂ ` ) "/\" (b₃ ` )

proof end;

theorem Th52: :: LATTICES:52

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ holds
( b₂ "/\" b₃ = Bottom b₁ iff b₂ [= b₃ ` )

proof end;

theorem Th53: :: LATTICES:53

for b₁ being B_Lattice
for b₂, b₃ being Element of b₁ st b₂ [= b₃ holds
b₃ ` [= b₂ `

proof end;