---

Step * of Lemma dfan-implies-twkl!

∀[T:Type]. ((∃size:ℕ. T ~ ℕsize) ⇒ Fan_d(T) ⇒ WKL!(T))
BY
{ (InstLemma `bar-separation-implies-twkl!` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN (D 0 THENA Auto)
   THEN BHyp -2
   THEN Auto) }

1
1. [T] : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T) ⇒ (∀A:(T List) ⟶ ℙ. (dbar(T;A) ⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))))) ⇒ WKL!(T)
4. Fan_d(T)
⊢ BarSep(T;T)

2
1. T : Type
2. ∃size:ℕ. T ~ ℕsize
3. BarSep(T;T) ⇒ (∀A:(T List) ⟶ ℙ. (dbar(T;A) ⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))))) ⇒ WKL!(T)
4. Fan_d(T)
5. A : (T List) ⟶ ℙ
6. dbar(T;A)
⊢ ¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size)  {}\mRightarrow{}  Fan\_d(T)  {}\mRightarrow{}  WKL!(T))


By

---

Latex:
(InstLemma  `bar-separation-implies-twkl!`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  BHyp  -2
  THEN  Auto)

---

Home Index