---

Step * 1 of Lemma mk-lattice_wf


1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. ∀[a,b:T].  (m[a;b] = m[b;a] ∈ T)
5. ∀[a,b:T].  (j[a;b] = j[b;a] ∈ T)
6. ∀[a,b,c:T].  (m[a;m[b;c]] = m[m[a;b];c] ∈ T)
7. ∀[a,b,c:T].  (j[a;j[b;c]] = j[j[a;b];c] ∈ T)
8. ∀[a,b:T].  (j[a;m[a;b]] = a ∈ T)
9. ∀[a,b:T].  (m[a;j[a;b]] = a ∈ T)
⊢ λx.x["Point" := T]["meet" := m]["join" := j] ∈ {l:LatticeStructure| lattice-axioms(l)} 
BY
{ (MemTypeCD THEN Auto) }

1
1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. ∀[a,b:T].  (m[a;b] = m[b;a] ∈ T)
5. ∀[a,b:T].  (j[a;b] = j[b;a] ∈ T)
6. ∀[a,b,c:T].  (m[a;m[b;c]] = m[m[a;b];c] ∈ T)
7. ∀[a,b,c:T].  (j[a;j[b;c]] = j[j[a;b];c] ∈ T)
8. ∀[a,b:T].  (j[a;m[a;b]] = a ∈ T)
9. ∀[a,b:T].  (m[a;j[a;b]] = a ∈ T)
⊢ λx.x["Point" := T]["meet" := m]["join" := j] ∈ LatticeStructure

2
.....set predicate..... 
1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. ∀[a,b:T].  (m[a;b] = m[b;a] ∈ T)
5. ∀[a,b:T].  (j[a;b] = j[b;a] ∈ T)
6. ∀[a,b,c:T].  (m[a;m[b;c]] = m[m[a;b];c] ∈ T)
7. ∀[a,b,c:T].  (j[a;j[b;c]] = j[j[a;b];c] ∈ T)
8. ∀[a,b:T].  (j[a;m[a;b]] = a ∈ T)
9. ∀[a,b:T].  (m[a;j[a;b]] = a ∈ T)
⊢ lattice-axioms(λx.x["Point" := T]["meet" := m]["join" := j])

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
3.  j  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
4.  \mforall{}[a,b:T].    (m[a;b]  =  m[b;a])
5.  \mforall{}[a,b:T].    (j[a;b]  =  j[b;a])
6.  \mforall{}[a,b,c:T].    (m[a;m[b;c]]  =  m[m[a;b];c])
7.  \mforall{}[a,b,c:T].    (j[a;j[b;c]]  =  j[j[a;b];c])
8.  \mforall{}[a,b:T].    (j[a;m[a;b]]  =  a)
9.  \mforall{}[a,b:T].    (m[a;j[a;b]]  =  a)
\mvdash{}  \mlambda{}x.x["Point"  :=  T]["meet"  :=  m]["join"  :=  j]  \mmember{}  \{l:LatticeStructure|  lattice-axioms(l)\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index