---

Step * of Lemma init0-baire-diff-from

∀a:ℕ ⟶ ℕ. ∀n:ℕ.  (0 < n ⇒ init0(a) ⇒ init0(baire-diff-from(a;n)))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``init0 baire-diff-from`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n:\mBbbN{}.    (0  <  n  {}\mRightarrow{}  init0(a)  {}\mRightarrow{}  init0(baire-diff-from(a;n)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``init0  baire-diff-from``  0  THEN  AutoSplit)

---

Home Index