---

Step * of Lemma evodd-enum-surjection

Surj(ℕ;b:𝔹 × (pw-evenodd() b);λn.evodd-enum(n))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN Reduce 0 THEN RepeatFor 2 (MoveToConcl (-1))) }

1
∀b1:𝔹. ∀b2:pw-evenodd() b1.  ∃a:ℕ. (evodd-enum(a) = <b1, b2> ∈ (b:𝔹 × (pw-evenodd() b)))

---

Latex:

---

Latex:
Surj(\mBbbN{};b:\mBbbB{}  \mtimes{}  (pw-evenodd()  b);\mlambda{}n.evodd-enum(n))


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  Reduce  0  THEN  RepeatFor  2  (MoveToConcl  (-1)))

---

Home Index