---

Step * of Lemma all-large_wf

∀[P:ℕ ⟶ ℙ]. (∀large(n).P[n] ∈ ℙ)
BY
{ (Unfold `all-large` 0 THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (\mforall{}large(n).P[n]  \mmember{}  \mBbbP{})


By

---

Latex:
(Unfold  `all-large`  0  THEN  Auto')

---

Home Index