:: LATTICE2 semantic presentation

theorem Th1: :: LATTICE2:1

canceled;

theorem Th2: :: LATTICE2:2

for b₁ being set
for b₂ being non empty set
for b₃ being Subset of b₁
for b₄ being Function of b₁,b₂ holds dom (b₄ | b₃) = b₃

proof end;

theorem Th3: :: LATTICE2:3

canceled;

theorem Th4: :: LATTICE2:4

canceled;

theorem Th5: :: LATTICE2:5

for b₁ being set
for b₂ being non empty set
for b₃ being Subset of b₁
for b₄, b₅ being Function of b₁,b₂ holds
( b₄ | b₃ = b₅ | b₃ iff for b₆ being Element of b₁ st b₆ in b₃ holds
b₅ . b₆ = b₄ . b₆ )

proof end;

theorem Th6: :: LATTICE2:6

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being Function of b₁,b₂
for b₅ being set holds b₃ +* (b₄ | b₅) is Function of b₁,b₂

proof end;

theorem Th7: :: LATTICE2:7

for b₁ being set
for b₂ being non empty set
for b₃ being Subset of b₁
for b₄, b₅ being Function of b₁,b₂ holds (b₄ | b₃) +* b₅ = b₅

proof end;

theorem Th8: :: LATTICE2:8

for b₁, b₂ being Function st b₂ <= b₁ holds
b₁ +* b₂ = b₁

proof end;

theorem Th9: :: LATTICE2:9

for b₁ being set
for b₂ being non empty set
for b₃ being Subset of b₁
for b₄ being Function of b₁,b₂ holds b₄ +* (b₄ | b₃) = b₄

proof end;

theorem Th10: :: LATTICE2:10

for b₁ being set
for b₂ being non empty set
for b₃ being Subset of b₁
for b₄, b₅ being Function of b₁,b₂ st ( for b₆ being Element of b₁ st b₆ in b₃ holds
b₄ . b₆ = b₅ . b₆ ) holds
b₅ +* (b₄ | b₃) = b₅

proof end;

theorem Th11: :: LATTICE2:11

canceled;

theorem Th12: :: LATTICE2:12

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being Function of b₁,b₂
for b₅ being Finite_Subset of b₁ holds (b₃ | b₅) +* b₄ = b₄

proof end;

theorem Th13: :: LATTICE2:13

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Finite_Subset of b₁ holds dom (b₃ | b₄) = b₄

proof end;

theorem Th14: :: LATTICE2:14

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being Function of b₁,b₂
for b₅ being Finite_Subset of b₁ st ( for b₆ being Element of b₁ st b₆ in b₅ holds
b₃ . b₆ = b₄ . b₆ ) holds
b₄ +* (b₃ | b₅) = b₄

proof end;

theorem Th15: :: LATTICE2:15

canceled;

theorem Th16: :: LATTICE2:16

for b₁ being set
for b₂ being non empty set
for b₃, b₄ being Function of b₁,b₂
for b₅ being Finite_Subset of b₁ st b₃ | b₅ = b₄ | b₅ holds
b₃ .: b₅ = b₄ .: b₅

proof end;

definition

let c₁ be non empty set ;
let c₂, c₃ be BinOp of c₁;
pred c₂ absorbs c₃ means :Def1: :: LATTICE2:def 1
for b₁, b₂ being Element of a₁ holds a₂ . b₁,(a₃ . b₁,b₂) = b₁;

end;

:: deftheorem Def1 defines absorbs LATTICE2:def 1 :

notation

let c₁ be non empty set ;
let c₂, c₃ be BinOp of c₁;
antonym c₂ doesn't_absorb c₃ for c₂ absorbs c₃;

end;

theorem Th17: :: LATTICE2:17

for b₁ being non empty LattStr st the L_join of b₁ is commutative & the L_join of b₁ is associative & the L_meet of b₁ is commutative & the L_meet of b₁ is associative & the L_join of b₁ absorbs the L_meet of b₁ & the L_meet of b₁ absorbs the L_join of b₁ holds
b₁ is Lattice-like

proof end;

definition

let c₁ be LattStr ;
func c₁ .: -> strict LattStr equals :: LATTICE2:def 2
LattStr(# the carrier of a₁,the L_meet of a₁,the L_join of a₁ #);
correctness ;

end;

:: deftheorem Def2 defines .: LATTICE2:def 2 :

registration

let c₁ be non empty LattStr ;
cluster a₁ .: -> non empty strict ;
coherence ;

end;

theorem Th18: :: LATTICE2:18

for b₁ being non empty LattStr holds
( the carrier of b₁ = the carrier of (b₁ .: ) & the L_join of b₁ = the L_meet of (b₁ .: ) & the L_meet of b₁ = the L_join of (b₁ .: ) ) ;

theorem Th19: :: LATTICE2:19

for b₁ being non empty strict LattStr holds (b₁ .: ) .: = b₁ ;

theorem Th20: :: LATTICE2:20

canceled;

theorem Th21: :: LATTICE2:21

for b₁ being Lattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₂ "\/" b₃ = b₃ ) holds
b₂ = Bottom b₁

proof end;

theorem Th22: :: LATTICE2:22

for b₁ being Lattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds the L_join of b₁ . b₂,b₃ = b₃ ) holds
b₂ = Bottom b₁

proof end;

theorem Th23: :: LATTICE2:23

canceled;

theorem Th24: :: LATTICE2:24

for b₁ being Lattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds b₂ "/\" b₃ = b₃ ) holds
b₂ = Top b₁

proof end;

theorem Th25: :: LATTICE2:25

for b₁ being Lattice
for b₂ being Element of b₁ st ( for b₃ being Element of b₁ holds the L_meet of b₁ . b₂,b₃ = b₃ ) holds
b₂ = Top b₁

proof end;

theorem Th26: :: LATTICE2:26

for b₁ being Lattice holds the L_join of b₁ is idempotent

proof end;

theorem Th27: :: LATTICE2:27

for b₁ being non empty join-commutative \/-SemiLattStr holds the L_join of b₁ is commutative

proof end;

theorem Th28: :: LATTICE2:28

for b₁ being Lattice st the L_join of b₁ has_a_unity holds
Bottom b₁ = the_unity_wrt the L_join of b₁

proof end;

theorem Th29: :: LATTICE2:29

for b₁ being non empty join-associative \/-SemiLattStr holds the L_join of b₁ is associative

proof end;

theorem Th30: :: LATTICE2:30

for b₁ being Lattice holds the L_meet of b₁ is idempotent

proof end;

theorem Th31: :: LATTICE2:31

for b₁ being non empty meet-commutative /\-SemiLattStr holds the L_meet of b₁ is commutative

proof end;

theorem Th32: :: LATTICE2:32

for b₁ being non empty meet-associative /\-SemiLattStr holds the L_meet of b₁ is associative

proof end;

registration

let c₁ be non empty join-commutative \/-SemiLattStr ;
cluster the L_join of a₁ -> commutative ;
coherence by Th27;

end;

registration

let c₁ be non empty join-associative \/-SemiLattStr ;
cluster the L_join of a₁ -> associative ;
coherence by Th29;

end;

registration

let c₁ be non empty meet-commutative /\-SemiLattStr ;
cluster the L_meet of a₁ -> commutative ;
coherence by Th31;

end;

registration

let c₁ be non empty meet-associative /\-SemiLattStr ;
cluster the L_meet of a₁ -> associative ;
coherence by Th32;

end;

theorem Th33: :: LATTICE2:33

for b₁ being Lattice st the L_meet of b₁ has_a_unity holds
Top b₁ = the_unity_wrt the L_meet of b₁

proof end;

theorem Th34: :: LATTICE2:34

for b₁ being Lattice holds the L_join of b₁ is_distributive_wrt the L_join of b₁

proof end;

theorem Th35: :: LATTICE2:35

for b₁ being Lattice st b₁ is D_Lattice holds
the L_join of b₁ is_distributive_wrt the L_meet of b₁

proof end;

theorem Th36: :: LATTICE2:36

for b₁ being Lattice st the L_join of b₁ is_distributive_wrt the L_meet of b₁ holds
b₁ is distributive

proof end;

theorem Th37: :: LATTICE2:37

for b₁ being Lattice st b₁ is D_Lattice holds
the L_meet of b₁ is_distributive_wrt the L_join of b₁

proof end;

theorem Th38: :: LATTICE2:38

for b₁ being Lattice st the L_meet of b₁ is_distributive_wrt the L_join of b₁ holds
b₁ is distributive

proof end;

theorem Th39: :: LATTICE2:39

for b₁ being Lattice holds the L_meet of b₁ is_distributive_wrt the L_meet of b₁

proof end;

theorem Th40: :: LATTICE2:40

for b₁ being Lattice holds the L_join of b₁ absorbs the L_meet of b₁

proof end;

theorem Th41: :: LATTICE2:41

for b₁ being Lattice holds the L_meet of b₁ absorbs the L_join of b₁

proof end;

definition

let c₁ be non empty set ;
let c₂ be Lattice;
let c₃ be Finite_Subset of c₁;
let c₄ be Function of c₁,the carrier of c₂;
func FinJoin c₃,c₄ -> Element of a₂ equals :: LATTICE2:def 3
the L_join of a₂ $$ a₃,a₄;
correctness ;
func FinMeet c₃,c₄ -> Element of a₂ equals :: LATTICE2:def 4
the L_meet of a₂ $$ a₃,a₄;
correctness ;

end;

:: deftheorem Def3 defines FinJoin LATTICE2:def 3 :

:: deftheorem Def4 defines FinMeet LATTICE2:def 4 :

theorem Th42: :: LATTICE2:42

canceled;

theorem Th43: :: LATTICE2:43

for b₁ being Lattice
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being Finite_Subset of b₂
for b₅ being Function of b₂,the carrier of b₁ st b₃ in b₄ holds
b₅ . b₃ [= FinJoin b₄,b₅

proof end;

theorem Th44: :: LATTICE2:44

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Finite_Subset of b₃
for b₅ being Function of b₃,the carrier of b₁ st ex b₆ being Element of b₃ st
( b₆ in b₄ & b₂ [= b₅ . b₆ ) holds
b₂ [= FinJoin b₄,b₅

proof end;

theorem Th45: :: LATTICE2:45

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Finite_Subset of b₃
for b₅ being Function of b₃,the carrier of b₁ st ( for b₆ being Element of b₃ st b₆ in b₄ holds
b₅ . b₆ = b₂ ) & b₄ <> {} holds
FinJoin b₄,b₅ = b₂

proof end;

theorem Th46: :: LATTICE2:46

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Finite_Subset of b₃
for b₅ being Function of b₃,the carrier of b₁ st FinJoin b₄,b₅ [= b₂ holds
for b₆ being Element of b₃ st b₆ in b₄ holds
b₅ . b₆ [= b₂

proof end;

theorem Th47: :: LATTICE2:47

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Finite_Subset of b₃
for b₅ being Function of b₃,the carrier of b₁ st b₄ <> {} & ( for b₆ being Element of b₃ st b₆ in b₄ holds
b₅ . b₆ [= b₂ ) holds
FinJoin b₄,b₅ [= b₂

proof end;

theorem Th48: :: LATTICE2:48

for b₁ being Lattice
for b₂ being non empty set
for b₃ being Finite_Subset of b₂
for b₄, b₅ being Function of b₂,the carrier of b₁ st b₃ <> {} & ( for b₆ being Element of b₂ st b₆ in b₃ holds
b₄ . b₆ [= b₅ . b₆ ) holds
FinJoin b₃,b₄ [= FinJoin b₃,b₅

proof end;

theorem Th49: :: LATTICE2:49

for b₁ being Lattice
for b₂ being non empty set
for b₃ being Finite_Subset of b₂
for b₄, b₅ being Function of b₂,the carrier of b₁ st b₃ <> {} & b₄ | b₃ = b₅ | b₃ holds
FinJoin b₃,b₄ = FinJoin b₃,b₅

proof end;

theorem Th50: :: LATTICE2:50

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Finite_Subset of b₃
for b₅ being Function of b₃,the carrier of b₁ st b₄ <> {} holds
b₂ "\/" (FinJoin b₄,b₅) = FinJoin b₄,(the L_join of b₁ [;] b₂,b₅)

proof end;

registration

let c₁ be Lattice;
cluster a₁ .: -> non empty strict Lattice-like ;
coherence

proof end;

end;

theorem Th51: :: LATTICE2:51

for b₁ being non empty set
for b₂ being Lattice
for b₃ being Finite_Subset of b₁
for b₄ being Function of b₁,the carrier of b₂
for b₅ being Function of b₁,the carrier of (b₂ .: ) st b₄ = b₅ holds
( FinJoin b₃,b₄ = FinMeet b₃,b₅ & FinMeet b₃,b₄ = FinJoin b₃,b₅ ) ;

theorem Th52: :: LATTICE2:52

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄, b₅ being Element of (b₁ .: ) st b₂ = b₄ & b₃ = b₅ holds
( b₂ "/\" b₃ = b₄ "\/" b₅ & b₂ "\/" b₃ = b₄ "/\" b₅ ) ;

theorem Th53: :: LATTICE2:53

for b₁ being Lattice
for b₂, b₃ being Element of b₁ st b₂ [= b₃ holds
for b₄, b₅ being Element of (b₁ .: ) st b₂ = b₄ & b₃ = b₅ holds
b₅ [= b₄

proof end;

theorem Th54: :: LATTICE2:54

for b₁ being Lattice
for b₂, b₃ being Element of b₁
for b₄, b₅ being Element of (b₁ .: ) st b₄ [= b₅ & b₂ = b₄ & b₃ = b₅ holds
b₃ [= b₂

proof end;

theorem Th55: :: LATTICE2:55

for b₁ being Lattice
for b₂ being non empty set
for b₃ being Element of b₂
for b₄ being Finite_Subset of b₂
for b₅ being Function of b₂,the carrier of b₁ st b₃ in b₄ holds
FinMeet b₄,b₅ [= b₅ . b₃

proof end;

theorem Th56: :: LATTICE2:56

proof end;

theorem Th57: :: LATTICE2:57

proof end;

theorem Th58: :: LATTICE2:58

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Finite_Subset of b₃
for b₅ being Function of b₃,the carrier of b₁ st b₄ <> {} holds
b₂ "/\" (FinMeet b₄,b₅) = FinMeet b₄,(the L_meet of b₁ [;] b₂,b₅)

proof end;

theorem Th59: :: LATTICE2:59

for b₁ being Lattice
for b₂ being Element of b₁
for b₃ being non empty set
for b₄ being Finite_Subset of b₃
for b₅ being Function of b₃,the carrier of b₁ st b₂ [= FinMeet b₄,b₅ holds
for b₆ being Element of b₃ st b₆ in b₄ holds
b₂ [= b₅ . b₆

proof end;

theorem Th60: :: LATTICE2:60

for b₁ being Lattice
for b₂ being non empty set
for b₃ being Finite_Subset of b₂
for b₄, b₅ being Function of b₂,the carrier of b₁ st b₃ <> {} & b₄ | b₃ = b₅ | b₃ holds
FinMeet b₃,b₄ = FinMeet b₃,b₅

proof end;

theorem Th61: :: LATTICE2:61

proof end;

theorem Th62: :: LATTICE2:62

proof end;

theorem Th63: :: LATTICE2:63

for b₁ being Lattice holds
( b₁ is lower-bounded iff b₁ .: is upper-bounded )

proof end;

theorem Th64: :: LATTICE2:64

for b₁ being Lattice holds
( b₁ is upper-bounded iff b₁ .: is lower-bounded )

proof end;

theorem Th65: :: LATTICE2:65

for b₁ being Lattice holds
( b₁ is D_Lattice iff b₁ .: is D_Lattice )

proof end;

theorem Th66: :: LATTICE2:66

for b₁ being 0_Lattice holds Bottom b₁ is_a_unity_wrt the L_join of b₁

proof end;

theorem Th67: :: LATTICE2:67

for b₁ being 0_Lattice holds the L_join of b₁ has_a_unity

proof end;

theorem Th68: :: LATTICE2:68

for b₁ being 0_Lattice holds Bottom b₁ = the_unity_wrt the L_join of b₁

proof end;

theorem Th69: :: LATTICE2:69

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being 0_Lattice
for b₄, b₅ being Function of b₁,the carrier of b₃ st b₄ | b₂ = b₅ | b₂ holds
FinJoin b₂,b₄ = FinJoin b₂,b₅

proof end;

theorem Th70: :: LATTICE2:70

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being 0_Lattice
for b₄ being Function of b₁,the carrier of b₃
for b₅ being Element of b₃ st ( for b₆ being Element of b₁ st b₆ in b₂ holds
b₄ . b₆ [= b₅ ) holds
FinJoin b₂,b₄ [= b₅

proof end;

theorem Th71: :: LATTICE2:71

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being 0_Lattice
for b₄, b₅ being Function of b₁,the carrier of b₃ st ( for b₆ being Element of b₁ st b₆ in b₂ holds
b₄ . b₆ [= b₅ . b₆ ) holds
FinJoin b₂,b₄ [= FinJoin b₂,b₅

proof end;

theorem Th72: :: LATTICE2:72

for b₁ being 1_Lattice holds Top b₁ is_a_unity_wrt the L_meet of b₁

proof end;

theorem Th73: :: LATTICE2:73

for b₁ being 1_Lattice holds the L_meet of b₁ has_a_unity

proof end;

theorem Th74: :: LATTICE2:74

for b₁ being 1_Lattice holds Top b₁ = the_unity_wrt the L_meet of b₁

proof end;

theorem Th75: :: LATTICE2:75

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being 1_Lattice
for b₄, b₅ being Function of b₁,the carrier of b₃ st b₄ | b₂ = b₅ | b₂ holds
FinMeet b₂,b₄ = FinMeet b₂,b₅

proof end;

theorem Th76: :: LATTICE2:76

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being 1_Lattice
for b₄ being Function of b₁,the carrier of b₃
for b₅ being Element of b₃ st ( for b₆ being Element of b₁ st b₆ in b₂ holds
b₅ [= b₄ . b₆ ) holds
b₅ [= FinMeet b₂,b₄

proof end;

theorem Th77: :: LATTICE2:77

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being 1_Lattice
for b₄, b₅ being Function of b₁,the carrier of b₃ st ( for b₆ being Element of b₁ st b₆ in b₂ holds
b₄ . b₆ [= b₅ . b₆ ) holds
FinMeet b₂,b₄ [= FinMeet b₂,b₅

proof end;

theorem Th78: :: LATTICE2:78

for b₁ being 0_Lattice holds Bottom b₁ = Top (b₁ .: )

proof end;

theorem Th79: :: LATTICE2:79

for b₁ being 1_Lattice holds Top b₁ = Bottom (b₁ .: )

proof end;

definition

mode D0_Lattice is distributive lower-bounded Lattice;

end;

theorem Th80: :: LATTICE2:80

for b₁ being D0_Lattice holds the L_meet of b₁ is_distributive_wrt the L_join of b₁ by Th37;

theorem Th81: :: LATTICE2:81

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being D0_Lattice
for b₄ being Function of b₁,the carrier of b₃
for b₅ being Element of b₃ holds the L_meet of b₃ . b₅,(FinJoin b₂,b₄) = FinJoin b₂,(the L_meet of b₃ [;] b₅,b₄)

proof end;

theorem Th82: :: LATTICE2:82

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being D0_Lattice
for b₄, b₅ being Function of b₁,the carrier of b₃
for b₆ being Element of b₃ st ( for b₇ being Element of b₁ st b₇ in b₂ holds
b₄ . b₇ = b₆ "/\" (b₅ . b₇) ) holds
b₆ "/\" (FinJoin b₂,b₅) = FinJoin b₂,b₄

proof end;

theorem Th83: :: LATTICE2:83

for b₁ being non empty set
for b₂ being Finite_Subset of b₁
for b₃ being D0_Lattice
for b₄ being Function of b₁,the carrier of b₃
for b₅ being Element of b₃ holds b₅ "/\" (FinJoin b₂,b₄) = FinJoin b₂,(the L_meet of b₃ [;] b₅,b₄) by Th81;

definition

let c₁ be Lattice;
canceled;
attr a₁ is Heyting means :Def6: :: LATTICE2:def 6
( a₁ is implicative & a₁ is lower-bounded );

end;

:: deftheorem Def5 LATTICE2:def 5 :

:: deftheorem Def6 defines Heyting LATTICE2:def 6 :

registration

cluster Heyting LattStr ;
existence

proof end;

end;

registration

cluster Heyting -> lower-bounded implicative LattStr ;
coherence by Def6;
cluster lower-bounded implicative -> Heyting LattStr ;
coherence by Def6;

end;

definition

mode H_Lattice is Heyting Lattice;

end;

registration

cluster strict lower-bounded implicative Heyting LattStr ;
existence

proof end;

end;

theorem Th84: :: LATTICE2:84

for b₁ being 0_Lattice holds
( b₁ is H_Lattice iff for b₂, b₃ being Element of b₁ ex b₄ being Element of b₁ st
( b₂ "/\" b₄ [= b₃ & ( for b₅ being Element of b₁ st b₂ "/\" b₅ [= b₃ holds
b₅ [= b₄ ) ) )

proof end;

theorem Th85: :: LATTICE2:85

for b₁ being Lattice holds
( b₁ is finite iff b₁ .: is finite )

proof end;

Lemma54: for b₁ being Lattice st b₁ is finite holds
b₁ is lower-bounded

proof end;

Lemma55: for b₁ being Lattice st b₁ is finite holds
b₁ is upper-bounded

proof end;

registration

cluster finite -> lower-bounded LattStr ;
coherence by Lemma54;
cluster finite -> upper-bounded LattStr ;
coherence by Lemma55;

end;

registration

cluster finite -> bounded LattStr ;
coherence

proof end;

end;

registration

cluster finite distributive -> lower-bounded implicative Heyting LattStr ;
coherence

proof end;

end;