---

Step * of Lemma fan-iff-wkl!

Fan ⇐⇒ WKL!
BY
{ ((RWO "fan-iff-dfan-bool wkl!-iff-twkl!-bool" 0 THENA Auto) THEN InstLemma `dfan-iff-twkl!` [⌜𝔹⌝]⋅ THEN Auto) }

1
.....antecedent..... 
∃k:ℕ. 𝔹 ~ ℕk

---

Latex:

---

Latex:
Fan  \mLeftarrow{}{}\mRightarrow{}  WKL!


By

---

Latex:
((RWO  "fan-iff-dfan-bool  wkl!-iff-twkl!-bool"  0  THENA  Auto)
  THEN  InstLemma  `dfan-iff-twkl!`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index