---

Step * of Lemma m-not-reg_wf

∀[X:Type]. ∀[d:metric(X)]. ∀[n:ℕ]. ∀[s:ℕn + 1 ⟶ X].  (m-not-reg(d;s;n) ∈ 𝔹)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  +  1  {}\mrightarrow{}  X].    (m-not-reg(d;s;n)  \mmember{}  \mBbbB{})


By

---

Latex:
ProveWfLemma

---

Home Index