---

Step * 1 of Lemma equipollent-nat-list-as-product


1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. ∀n:ℕ. ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
⊢ ℕ ~ k:ℕ × (ℕ^k)
BY
{ xxx(With λn.if (n =z 0) then <0, ⋅> else let n1,n2 = coded-pair(n - 1) in <n1 + 1, f n1 n2> fi  (D 0)⋅ THEN Auto)xxx }

1
1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. ∀n:ℕ. ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
⊢ Bij(ℕ;k:ℕ × (ℕ^k);λn.if (n =z 0) then <0, ⋅> else let n1,n2 = coded-pair(n - 1) in <n1 + 1, f n1 n2> fi )

---

Latex:

---

Latex:

1.  f  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n  +  1)
2.  \mforall{}n:\mBbbN{}.  \mexists{}g:(\mBbbN{}\^{}n  +  1)  {}\mrightarrow{}  \mBbbN{}.  InvFuns(\mBbbN{};(\mBbbN{}\^{}n  +  1);f  n;g)
\mvdash{}  \mBbbN{}  \msim{}  k:\mBbbN{}  \mtimes{}  (\mBbbN{}\^{}k)


By

---

Latex:
xxx(With  \mlambda{}n.if  (n  =\msubz{}  0)  then  ɘ,  \mcdot{}>  else  let  n1,n2  =  coded-pair(n  -  1)  in  <n1  +  1,  f  n1  n2>  fi 
          (D  0)\mcdot{}
        THEN  Auto
        )xxx

---

Home Index