---

Step * of Lemma free-dl-le

∀[T:Type]. ∀eq:EqDecider(T). ∀x,y:Point(free-dist-lattice(T; eq)).  (x ≤ y ⇐⇒ fset-ac-le(eq;x;y))
BY
{ Intros }

1
1. [T] : Type
2. eq : EqDecider(T)@i
3. x : Point(free-dist-lattice(T; eq))@i
4. y : Point(free-dist-lattice(T; eq))@i
⊢ x ≤ y ⇐⇒ fset-ac-le(eq;x;y)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}x,y:Point(free-dist-lattice(T;  eq)).    (x  \mleq{}  y  \mLeftarrow{}{}\mRightarrow{}  fset-ac-le(eq;x;y))


By

---

Latex:
Intros

---

Home Index