---

Step * of Lemma surjection-cantor-finite-branching

∀b:ℕ ⟶ ℕ+. ∃F:(ℕ ⟶ 𝔹) ⟶ n:ℕ ⟶ ℕb n. Surj(ℕ ⟶ 𝔹;n:ℕ ⟶ ℕb n;F)
BY
{ xxx(Auto
      THEN With ⌜λg,n. cantor-to-fb(b;g;n)⌝ (D 0)⋅
      THEN Auto
      THEN D 0
      THEN Auto
      THEN RenameVar `f' (-1)
      THEN (With ⌜λk.fb-to-cantor(b;f;k)⌝ (D 0)⋅ THENA Auto)
      THEN Reduce 0
      THEN (Ext THENA Auto)
      THEN Reduce 0)xxx }

1
1. b : ℕ ⟶ ℕ+
2. f : n:ℕ ⟶ ℕb n
3. x : ℕ
⊢ cantor-to-fb(b;λk.fb-to-cantor(b;f;k);x) = (f x) ∈ ℕb x

---

Latex:

---

Latex:
\mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}.  \mexists{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}b  n.  Surj(\mBbbN{}  {}\mrightarrow{}  \mBbbB{};n:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}b  n;F)


By

---

Latex:
xxx(Auto
        THEN  With  \mkleeneopen{}\mlambda{}g,n.  cantor-to-fb(b;g;n)\mkleeneclose{}  (D  0)\mcdot{}
        THEN  Auto
        THEN  D  0
        THEN  Auto
        THEN  RenameVar  `f'  (-1)
        THEN  (With  \mkleeneopen{}\mlambda{}k.fb-to-cantor(b;f;k)\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
        THEN  Reduce  0
        THEN  (Ext  THENA  Auto)
        THEN  Reduce  0)xxx

---

Home Index