---

Step * of Lemma equipollent-exp

∀n,b:ℕ.  ℕn ⟶ ℕb ~ ℕb^n
BY
{ InductionOnNat }

1
.....basecase..... 
∀b:ℕ. ℕ0 ⟶ ℕb ~ ℕb^0

2
.....upcase..... 
1. n : ℤ
2. [%1] : 0 < n
3. ∀b:ℕ. ℕn - 1 ⟶ ℕb ~ ℕb^(n - 1)
⊢ ∀b:ℕ. ℕn ⟶ ℕb ~ ℕb^n

---

Latex:

---

Latex:
\mforall{}n,b:\mBbbN{}.    \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}b  \msim{}  \mBbbN{}b\^{}n


By

---

Latex:
InductionOnNat

---

Home Index