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