---

Step * of Lemma nwkl!-implies-fan

nWKL! ⇒ Fan
BY
{ ((RWO "fan-iff-dfan-bool nwkl!-iff-twkl!-bool" 0 THENA Auto) THEN Auto THEN BLemma `twkl!-implies-dfan` ⋅ THEN Auto) }

1
1. WKL!(𝔹)@i'
⊢ ∃k:ℕ. 𝔹 ~ ℕk

---

Latex:

---

Latex:
nWKL!  {}\mRightarrow{}  Fan


By

---

Latex:
((RWO  "fan-iff-dfan-bool  nwkl!-iff-twkl!-bool"  0  THENA  Auto)
  THEN  Auto
  THEN  BLemma  `twkl!-implies-dfan`  \mcdot{}
  THEN  Auto)

---

Home Index