---

Step * of Lemma p-mu_wf

∀[P:ℕ ⟶ 𝔹]. ∀[x:ℕ + Top].  (p-mu(P;x) ∈ ℙ)
BY
{ (Unfold `p-mu` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:\mBbbN{}  +  Top].    (p-mu(P;x)  \mmember{}  \mBbbP{})


By

---

Latex:
(Unfold  `p-mu`  0  THEN  Auto)

---

Home Index