---

Step * of Lemma not-canonicalizable-baire-to-nat

¬⇃(canonicalizable((ℕ ⟶ ℕ) ⟶ ℕ))
BY
{ (RWO "choice-iff-canonicalizable<" 0 THEN Auto) }

---

Latex:

---

Latex:
\mneg{}\00D9(canonicalizable((\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}))


By

---

Latex:
(RWO  "choice-iff-canonicalizable<"  0  THEN  Auto)

---

Home Index