---

Step * of Lemma init0-baire-eq-from

∀a:ℕ ⟶ ℕ. ∀n:ℕ.  (init0(a) ⇒ init0(baire_eq_from(a;n)))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``init0 baire_eq_from`` 0 THEN AutoSplit) }

1
1. a : ℕ ⟶ ℕ
2. n : ℕ
3. ¬0 < n
4. init0(a)
⊢ (a n) = 0 ∈ ℕ

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n:\mBbbN{}.    (init0(a)  {}\mRightarrow{}  init0(baire\_eq\_from(a;n)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``init0  baire\_eq\_from``  0  THEN  AutoSplit)

---

Home Index