---

Step * of Lemma equipollent-nat-powered2

∃f:n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1). ∀n:ℕ. Bij(ℕ;(ℕ^n + 1);f n)
BY
{ (Auto THEN InstLemma `equipollent-nat-powered` [] THEN (RepUR ``equipollent`` 1 THEN RenameVar `g' 1)) }

1
1. g : ∀n:ℕ. ∃f:ℕ ⟶ (ℕ^n + 1). Bij(ℕ;(ℕ^n + 1);f)
⊢ ∃f:n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1). ∀n:ℕ. Bij(ℕ;(ℕ^n + 1);f n)

---

Latex:

---

Latex:
\mexists{}f:n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n  +  1).  \mforall{}n:\mBbbN{}.  Bij(\mBbbN{};(\mBbbN{}\^{}n  +  1);f  n)


By

---

Latex:
(Auto
  THEN  InstLemma  `equipollent-nat-powered`  []
  THEN  (RepUR  ``equipollent``  1  THEN  RenameVar  `g'  1))

---

Home Index