---

Step * of Lemma equipollent-nat-powered3

∃f:n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1). ∀n:ℕ. ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
BY
{ (Auto THEN InstLemma `equipollent-nat-powered2` [] THEN (D (-1) THEN InstConcl [⌜f⌝]⋅ THEN Auto)) }

1
1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. ∀n:ℕ. Bij(ℕ;(ℕ^n + 1);f n)
3. n : ℕ@i
⊢ ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  InstLemma  `equipollent-nat-powered2`  []  THEN  (D  (-1)  THEN  InstConcl  [\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THEN  Auto))

---

Home Index