---

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

∀[a:ℕ ⟶ ℕ]. ∀[n:ℕ].  (a = baire-diff-from(a;n) ∈ (ℕn ⟶ ℕ))
BY
{ ((UnivCD THENA Auto) THEN (Ext THENA Auto) THEN RepUR ``baire-diff-from`` 0 THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[n:\mBbbN{}].    (a  =  baire-diff-from(a;n))


By

---

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

---

Home Index