---

Step * 2 1 of Lemma equipollent-nat-powered


1. n : ℤ
2. [%1] : 0 < n
3. f : ℕ ⟶ (ℕ^n)
4. Bij(ℕ;(ℕ^n);f)
5. (n - 1) + 1 ~ n
6. ¬((n + 1) = 0 ∈ ℤ)
7. (n + 1) - 1 ~ n
⊢ ℕ ~ ℕ × (ℕ^n)
BY
{ ((With ⌜λn.let n1,n2 = coded-pair(n) in <n1, f n2>⌝ (D 0)⋅ THEN Auto)⋅
   THEN xxxBLemma `fun_with_inv_is_bij2`xxx
   THEN Auto
   THEN xxxFLemma `biject-inverse` [4]xxx
   THEN Auto
   THEN D (-1)) }

1
1. n : ℤ
2. [%1] : 0 < n
3. f : ℕ ⟶ (ℕ^n)
4. Bij(ℕ;(ℕ^n);f)
5. (n - 1) + 1 ~ n
6. ¬((n + 1) = 0 ∈ ℤ)
7. (n + 1) - 1 ~ n
8. g : (ℕ^n) ⟶ ℕ
9. (∀b:(ℕ^n). ((f (g b)) = b ∈ (ℕ^n))) ∧ (∀a:ℕ. ((g (f a)) = a ∈ ℕ))
⊢ ∃g:(ℕ × (ℕ^n)) ⟶ ℕ. InvFuns(ℕ;ℕ × (ℕ^n);λn.let n1,n2 = coded-pair(n) in <n1, f n2>;g)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  [\%1]  :  0  <  n
3.  f  :  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n)
4.  Bij(\mBbbN{};(\mBbbN{}\^{}n);f)
5.  (n  -  1)  +  1  \msim{}  n
6.  \mneg{}((n  +  1)  =  0)
7.  (n  +  1)  -  1  \msim{}  n
\mvdash{}  \mBbbN{}  \msim{}  \mBbbN{}  \mtimes{}  (\mBbbN{}\^{}n)


By

---

Latex:
((With  \mkleeneopen{}\mlambda{}n.let  n1,n2  =  coded-pair(n)  in  <n1,  f  n2>\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}
  THEN  xxxBLemma  `fun\_with\_inv\_is\_bij2`xxx
  THEN  Auto
  THEN  xxxFLemma  `biject-inverse`  [4]xxx
  THEN  Auto
  THEN  D  (-1))

---

Home Index