---

Step * 1 1 of Lemma equipollent-nat-powered2


1. g : ∀n:ℕ. ∃f:ℕ ⟶ (ℕ^n + 1). Bij(ℕ;(ℕ^n + 1);f)
2. n : ℕ@i
3. f : ℕ ⟶ (ℕ^n + 1)@i
4. v1 : Bij(ℕ;(ℕ^n + 1);f)@i
5. (g n) = <f, v1> ∈ (∃f:ℕ ⟶ (ℕ^n + 1). Bij(ℕ;(ℕ^n + 1);f))@i
⊢ Bij(ℕ;(ℕ^n + 1);fst(<f, v1>))
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  \mforall{}n:\mBbbN{}.  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n  +  1).  Bij(\mBbbN{};(\mBbbN{}\^{}n  +  1);f)
2.  n  :  \mBbbN{}@i
3.  f  :  \mBbbN{}  {}\mrightarrow{}  (\mBbbN{}\^{}n  +  1)@i
4.  v1  :  Bij(\mBbbN{};(\mBbbN{}\^{}n  +  1);f)@i
5.  (g  n)  =  <f,  v1>@i
\mvdash{}  Bij(\mBbbN{};(\mBbbN{}\^{}n  +  1);fst(<f,  v1>))


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index