---

Step * of Lemma cantor2baire2cantor

∀a:ℕ ⟶ 𝔹. (initF(a) ⇒ (baire2cantor(cantor2baire(a)) = a ∈ (ℕ ⟶ 𝔹)))
BY
{ ((UnivCD THENA Auto)
   THEN (Ext THENA Auto)
   THEN RepUR ``baire2cantor`` 0
   THEN RepUR ``cantor2baire`` 0
   THEN (Decide ⌜x = 0 ∈ ℕ⌝⋅ THENA Auto)) }

1
1. a : ℕ ⟶ 𝔹
2. initF(a)
3. x : ℕ
4. x = 0 ∈ ℕ
⊢ if (cantor2baire-aux(a;x) =z cantor2baire-aux(a;x-1)) then ff else tt fi  = a x

2
1. a : ℕ ⟶ 𝔹
2. initF(a)
3. x : ℕ
4. ¬(x = 0 ∈ ℕ)
⊢ if (cantor2baire-aux(a;x) =z cantor2baire-aux(a;x-1)) then ff else tt fi  = a x

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (initF(a)  {}\mRightarrow{}  (baire2cantor(cantor2baire(a))  =  a))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Ext  THENA  Auto)
  THEN  RepUR  ``baire2cantor``  0
  THEN  RepUR  ``cantor2baire``  0
  THEN  (Decide  \mkleeneopen{}x  =  0\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index