---

Step * 1 1 of Lemma equipollent-nat-powered3


1. f : n:ℕ ⟶ ℕ ⟶ (ℕ^n + 1)
2. ∀n:ℕ. Bij(ℕ;(ℕ^n + 1);f n)
3. n : ℕ@i
4. Bij(ℕ;(ℕ^n + 1);f n)
⊢ ∃g:(ℕ^n + 1) ⟶ ℕ. InvFuns(ℕ;(ℕ^n + 1);f n;g)
BY
{ (BLemma `biject-inverse2` THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n  +  1)
2.  \mforall{}n:\mBbbN{}.  Bij(\mBbbN{};(\mBbbN{}\^{}n  +  1);f  n)
3.  n  :  \mBbbN{}@i
4.  Bij(\mBbbN{};(\mBbbN{}\^{}n  +  1);f  n)
\mvdash{}  \mexists{}g:(\mBbbN{}\^{}n  +  1)  {}\mrightarrow{}  \mBbbN{}.  InvFuns(\mBbbN{};(\mBbbN{}\^{}n  +  1);f  n;g)


By

---

Latex:
(BLemma  `biject-inverse2`  THEN  Auto)

---

Home Index