---

Step * 1 2 of Lemma evodd-enum-surjection


1. b : 𝔹
2. x : pw-evenodd() b
3. ∃a:ℕ. (evodd-enum(a) = <b, x> ∈ (b:𝔹 × (pw-evenodd() b)))
⊢ ∃a:ℕ. (evodd-enum(a) = <¬bb, evodd-succ(x)> ∈ (b:𝔹 × (pw-evenodd() b)))
BY
{ (D -1 THEN With ⌜a + 1⌝ (D 0)⋅ THEN Auto) }

1
1. b : 𝔹
2. x : pw-evenodd() b
3. a : ℕ
4. evodd-enum(a) = <b, x> ∈ (b:𝔹 × (pw-evenodd() b))
⊢ evodd-enum(a + 1) = <¬bb, evodd-succ(x)> ∈ (b:𝔹 × (pw-evenodd() b))

---

Latex:

---

Latex:

1.  b  :  \mBbbB{}
2.  x  :  pw-evenodd()  b
3.  \mexists{}a:\mBbbN{}.  (evodd-enum(a)  =  <b,  x>)
\mvdash{}  \mexists{}a:\mBbbN{}.  (evodd-enum(a)  =  <\mneg{}\msubb{}b,  evodd-succ(x)>)


By

---

Latex:
(D  -1  THEN  With  \mkleeneopen{}a  +  1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index