---

Step * 1 of Lemma dfan-implies-twkl!


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)
BY
{ (BLemma `fan-implies-bar-sep` THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  \mexists{}size:\mBbbN{}.  T  \msim{}  \mBbbN{}size
3.  BarSep(T;T)
{}\mRightarrow{}  (\mforall{}A:(T  List)  {}\mrightarrow{}  \mBbbP{}.  (dbar(T;A)  {}\mRightarrow{}  (\mneg{}(down-closed(T;\mneg{}(A))  \mwedge{}  Unbounded(\mneg{}(A))))))
{}\mRightarrow{}  WKL!(T)
4.  Fan\_d(T)
\mvdash{}  BarSep(T;T)


By

---

Latex:
(BLemma  `fan-implies-bar-sep`  THEN  Auto)

---

Home Index