---

Step * of Lemma mu_wf

∀[f:ℕ ⟶ 𝔹]. mu(f) ∈ ℕ supposing ∃n:ℕ. (↑(f n))
BY
{ (ProveWfLemma THEN ParallelLast) }

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  mu(f)  \mmember{}  \mBbbN{}  supposing  \mexists{}n:\mBbbN{}.  (\muparrow{}(f  n))


By

---

Latex:
(ProveWfLemma  THEN  ParallelLast)

---

Home Index