---

Step * 2 of Lemma mk-general-bounded-dist-lattice_wf

.....set predicate..... 
1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. z : T
5. o : T
6. E : T ⟶ T ⟶ ℙ
7. EquivRel(T;x,y.E x y)
8. ∀[a,b:T].  (E m[a;b] m[b;a])
9. ∀[a,b:T].  (E j[a;b] j[b;a])
10. ∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c])
11. ∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c])
12. ∀[a,b:T].  (E j[a;m[a;b]] a)
13. ∀[a,b:T].  (E m[a;j[a;b]] a)
14. ∀[a:T]. (E m[a;o] a)
15. ∀[a:T]. (E j[a;z] a)
16. ∀[a,b,c:T].  (E m[a;j[b;c]] j[m[a;b];m[a;c]])
⊢ general-lattice-axioms(λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]["E" := E])
∧ (∀[a,b,c:Point(λx.x["Point" := T]["meet" := m]["join" := j]["0" := z]["1" := o]["E" := E])].
     a ∧ b ∨ c ≡ a ∧ b ∨ a ∧ c)
BY
{ (RepUR ``general-lattice-axioms lattice-point lattice-meet lattice-join`` 0
   THEN RepUR ``lattice-equiv lattice-0 lattice-1`` 0
   ) }

1
1. T : Type
2. m : T ⟶ T ⟶ T
3. j : T ⟶ T ⟶ T
4. z : T
5. o : T
6. E : T ⟶ T ⟶ ℙ
7. EquivRel(T;x,y.E x y)
8. ∀[a,b:T].  (E m[a;b] m[b;a])
9. ∀[a,b:T].  (E j[a;b] j[b;a])
10. ∀[a,b,c:T].  (E m[a;m[b;c]] m[m[a;b];c])
11. ∀[a,b,c:T].  (E j[a;j[b;c]] j[j[a;b];c])
12. ∀[a,b:T].  (E j[a;m[a;b]] a)
13. ∀[a,b:T].  (E m[a;j[a;b]] a)
14. ∀[a:T]. (E m[a;o] a)
15. ∀[a:T]. (E j[a;z] a)
16. ∀[a,b,c:T].  (E m[a;j[b;c]] j[m[a;b];m[a;c]])
⊢ (EquivRel(T;a,b.E a b)
∧ (∀[a,b:T].  (E (m a b) (m b a)))
∧ (∀[a,b:T].  (E (j a b) (j b a)))
∧ (∀[a,b,c:T].  (E (m a (m b c)) (m (m a b) c)))
∧ (∀[a,b,c:T].  (E (j a (j b c)) (j (j a b) c)))
∧ (∀[a,b:T].  (E (j a (m a b)) a))
∧ (∀[a,b:T].  (E (m a (j a b)) a))
∧ (∀[a:T]. (E (j a z) a))
∧ (∀[a:T]. (E (m a o) a)))
∧ (∀[a,b,c:T].  (E (m a (j b c)) (j (m a b) (m a c))))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  T  :  Type
2.  m  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
3.  j  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  T
4.  z  :  T
5.  o  :  T
6.  E  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
7.  EquivRel(T;x,y.E  x  y)
8.  \mforall{}[a,b:T].    (E  m[a;b]  m[b;a])
9.  \mforall{}[a,b:T].    (E  j[a;b]  j[b;a])
10.  \mforall{}[a,b,c:T].    (E  m[a;m[b;c]]  m[m[a;b];c])
11.  \mforall{}[a,b,c:T].    (E  j[a;j[b;c]]  j[j[a;b];c])
12.  \mforall{}[a,b:T].    (E  j[a;m[a;b]]  a)
13.  \mforall{}[a,b:T].    (E  m[a;j[a;b]]  a)
14.  \mforall{}[a:T].  (E  m[a;o]  a)
15.  \mforall{}[a:T].  (E  j[a;z]  a)
16.  \mforall{}[a,b,c:T].    (E  m[a;j[b;c]]  j[m[a;b];m[a;c]])
\mvdash{}  general-lattice-axioms(\mlambda{}x.x["Point"  :=  T]["meet"  :=  m]["join"  :=  j]["0"  :=  z]["1"  :=  o]["E"  :=  E])
\mwedge{}  (\mforall{}[a,b,c:Point(\mlambda{}x.x["Point"  :=  T]["meet"  :=  m]["join"  :=  j]["0"  :=  z]["1"  :=  o]["E"  :=  E])].
          a  \mwedge{}  b  \mvee{}  c  \mequiv{}  a  \mwedge{}  b  \mvee{}  a  \mwedge{}  c)


By

---

Latex:
(RepUR  ``general-lattice-axioms  lattice-point  lattice-meet  lattice-join``  0
  THEN  RepUR  ``lattice-equiv  lattice-0  lattice-1``  0
  )

---

Home Index