---

Step * of Lemma surject-nat-bool

∃g:ℕ ⟶ 𝔹. Surj(ℕ;𝔹;g)
BY
{ ((D 0 With ⌜λn.if (n =z 0) then ff else tt fi ⌝  THEN Auto)
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN BoolCase ⌜b⌝⋅
   THEN Auto) }

1
1. b : 𝔹
2. ↑b
⊢ ∃a:ℕ. if (a =z 0) then ff else tt fi  = tt

2
1. b : 𝔹
2. ¬↑b
⊢ ∃a:ℕ. if (a =z 0) then ff else tt fi  = ff

---

Latex:

---

Latex:
\mexists{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  Surj(\mBbbN{};\mBbbB{};g)


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}n.if  (n  =\msubz{}  0)  then  ff  else  tt  fi  \mkleeneclose{}    THEN  Auto)
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  BoolCase  \mkleeneopen{}b\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index