---

Step * of Lemma equipollent-nat-sequences

ℕ ~ k:ℕ × (ℕk ⟶ ℕ)
BY
{ (With ⌜λn.coded-seq(n)⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:
\mBbbN{}  \msim{}  k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  \mBbbN{})


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}n.coded-seq(n)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index