---

Step * of Lemma free-dlwc-point-subtype

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[Cs:T ⟶ fset(fset(T))].
  (Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x])) ⊆r Point(free-dist-lattice(T; eq)))
BY
{ (RWO "free-dl-point free-dlwc-point" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[Cs:T  {}\mrightarrow{}  fset(fset(T))].
    (Point(free-dist-lattice-with-constraints(T;eq;x.Cs[x]))  \msubseteq{}r  Point(free-dist-lattice(T;  eq)))


By

---

Latex:
(RWO  "free-dl-point  free-dlwc-point"  0  THEN  Auto)

---

Home Index