---

Step * of Lemma free-dl-1-join-irreducible

∀T:Type. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)).
  (x ∨ y = 1 ∈ Point(free-dist-lattice(T; eq))
  ⇐⇒ (x = 1 ∈ Point(free-dist-lattice(T; eq))) ∨ (y = 1 ∈ Point(free-dist-lattice(T; eq))))
BY
{ Auto }

1
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-dist-lattice(T; eq))
4. y : Point(free-dist-lattice(T; eq))
5. x ∨ y = 1 ∈ Point(free-dist-lattice(T; eq))
⊢ (x = 1 ∈ Point(free-dist-lattice(T; eq))) ∨ (y = 1 ∈ Point(free-dist-lattice(T; eq)))

2
1. T : Type
2. eq : EqDecider(T)
3. x : Point(free-dist-lattice(T; eq))
4. y : Point(free-dist-lattice(T; eq))
5. (x = 1 ∈ Point(free-dist-lattice(T; eq))) ∨ (y = 1 ∈ Point(free-dist-lattice(T; eq)))
⊢ x ∨ y = 1 ∈ Point(free-dist-lattice(T; eq))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}eq:EqDecider(T).  \mforall{}x,y:Point(free-dist-lattice(T;  eq)).    (x  \mvee{}  y  =  1  \mLeftarrow{}{}\mRightarrow{}  (x  =  1)  \mvee{}  (y  =  1))


By

---

Latex:
Auto

---

Home Index