---

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

ℕ ~ k:ℕ × (ℕ^k)
BY
{ xxx(Auto THEN InstLemma `equipollent-nat-powered3` [] THEN xxxxxxD (-1)xxxxxx)xxx }

1
1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. ∀n:ℕ. ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
⊢ ℕ ~ k:ℕ × (ℕ^k)

---

Latex:

---

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


By

---

Latex:
xxx(Auto  THEN  InstLemma  `equipollent-nat-powered3`  []  THEN  xxxxxxD  (-1)xxxxxx)xxx

---

Home Index