---

Step * of Lemma baire2cantor2baire

∀a:ℕ ⟶ ℕ. (init0(a) ⇒ increasing-sequence(a) ⇒ (cantor2baire(baire2cantor(a)) = a ∈ (ℕ ⟶ ℕ)))
BY
{ ((UnivCD THENA Auto) THEN (Ext THENA Auto) THEN NatInd (-1) THEN Auto) }

1
.....basecase..... 
1. a : ℕ ⟶ ℕ
2. init0(a)
3. increasing-sequence(a)
4. x : ℤ
⊢ (cantor2baire(baire2cantor(a)) 0) = (a 0) ∈ ℕ

2
.....upcase..... 
1. a : ℕ ⟶ ℕ
2. init0(a)
3. increasing-sequence(a)
4. x : ℤ
5. 0 < x
6. (cantor2baire(baire2cantor(a)) (x - 1)) = (a (x - 1)) ∈ ℕ
⊢ (cantor2baire(baire2cantor(a)) x) = (a x) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (init0(a)  {}\mRightarrow{}  increasing-sequence(a)  {}\mRightarrow{}  (cantor2baire(baire2cantor(a))  =  a))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (Ext  THENA  Auto)  THEN  NatInd  (-1)  THEN  Auto)

---

Home Index