---

Step * of Lemma eq-upto-baire-eq-from

∀a:ℕ ⟶ ℕ. ∀p,n:ℕ.  ((p ≤ n) ⇒ (a = baire_eq_from(a;n) ∈ (ℕp ⟶ ℕ)))
BY
{ ((UnivCD THENA Auto) THEN (Ext THENA Auto) THEN RepUR ``baire_eq_from`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}p,n:\mBbbN{}.    ((p  \mleq{}  n)  {}\mRightarrow{}  (a  =  baire\_eq\_from(a;n)))


By

---

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

---

Home Index