---

Step * of Lemma fan-iff-nwkl!

Fan ⇐⇒ nWKL!
BY
{ (Auto THEN (BLemma `fan-implies-nwkl!-using-PFan`⋅ ORELSE BLemma `nwkl!-implies-fan`) THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (BLemma  `fan-implies-nwkl!-using-PFan`\mcdot{}  ORELSE  BLemma  `nwkl!-implies-fan`)  THEN  Auto)

---

Home Index