---

Step * of Lemma dfan-iff-twkl!

∀T:Type. ((∃k:ℕ. T ~ ℕk) ⇒ (Fan_d(T) ⇐⇒ WKL!(T)))
BY
{ (Auto THEN ((BLemma `dfan-implies-twkl!` THEN Auto) ORELSE (BLemma `twkl!-implies-dfan` THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}T:Type.  ((\mexists{}k:\mBbbN{}.  T  \msim{}  \mBbbN{}k)  {}\mRightarrow{}  (Fan\_d(T)  \mLeftarrow{}{}\mRightarrow{}  WKL!(T)))


By

---

Latex:
(Auto  THEN  ((BLemma  `dfan-implies-twkl!`  THEN  Auto)  ORELSE  (BLemma  `twkl!-implies-dfan`  THEN  Auto)))

---

Home Index