---

Step * 2 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)
5. A : (T List) ⟶ ℙ
6. dbar(T;A)
⊢ ¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))
BY
{ (InstLemma `fan-implies-barred-not-unbounded` [⌜T⌝;⌜A⌝]⋅ 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)
5.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
6.  dbar(T;A)
\mvdash{}  \mneg{}(down-closed(T;\mneg{}(A))  \mwedge{}  Unbounded(\mneg{}(A)))


By

---

Latex:
(InstLemma  `fan-implies-barred-not-unbounded`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index