---

Step * of Lemma biject-bool-nsub2

∃f:𝔹 ⟶ ℕ2. Bij(𝔹;ℕ2;f)
BY
{ ((D 0 With ⌜λb.if b then 1 else 0 fi ⌝  THEN Auto) THEN RepeatFor 2 (D 0) THEN (Reduce 0 THENW Auto)) }

1
1. a1 : 𝔹
⊢ ∀a2:𝔹. ((if a1 then 1 else 0 fi  = if a2 then 1 else 0 fi  ∈ ℕ2) ⇒ a1 = a2)

2
1. b : ℕ2
⊢ ∃a:𝔹. (if a then 1 else 0 fi  = b ∈ ℕ2)

---

Latex:

---

Latex:
\mexists{}f:\mBbbB{}  {}\mrightarrow{}  \mBbbN{}2.  Bij(\mBbbB{};\mBbbN{}2;f)


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}b.if  b  then  1  else  0  fi  \mkleeneclose{}    THEN  Auto)
  THEN  RepeatFor  2  (D  0)
  THEN  (Reduce  0  THENW  Auto))

---

Home Index