---

Step * of Lemma quotient-dl_wf

∀[l:BoundedDistributiveLattice]. ∀[eq:Point(l) ⟶ Point(l) ⟶ ℙ].
  (l//x,y.eq[x;y] ∈ BoundedDistributiveLattice) supposing 
     ((∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∨ b;c ∨ d])) and 
     (∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∧ b;c ∧ d])) and 
     EquivRel(Point(l);x,y.eq[x;y]))
BY
{ Auto }

1
1. l : BoundedDistributiveLattice
2. eq : Point(l) ⟶ Point(l) ⟶ ℙ
3. EquivRel(Point(l);x,y.eq[x;y])
4. ∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∧ b;c ∧ d])
5. ∀a,c,b,d:Point(l).  (eq[a;c] ⇒ eq[b;d] ⇒ eq[a ∨ b;c ∨ d])
⊢ l//x,y.eq[x;y] ∈ BoundedDistributiveLattice

---

Latex:

---

Latex:
\mforall{}[l:BoundedDistributiveLattice].  \mforall{}[eq:Point(l)  {}\mrightarrow{}  Point(l)  {}\mrightarrow{}  \mBbbP{}].
    (l//x,y.eq[x;y]  \mmember{}  BoundedDistributiveLattice)  supposing 
          ((\mforall{}a,c,b,d:Point(l).    (eq[a;c]  {}\mRightarrow{}  eq[b;d]  {}\mRightarrow{}  eq[a  \mvee{}  b;c  \mvee{}  d]))  and 
          (\mforall{}a,c,b,d:Point(l).    (eq[a;c]  {}\mRightarrow{}  eq[b;d]  {}\mRightarrow{}  eq[a  \mwedge{}  b;c  \mwedge{}  d]))  and 
          EquivRel(Point(l);x,y.eq[x;y]))


By

---

Latex:
Auto

---

Home Index