---

Step * of Lemma fan-implies-barred-not-unbounded

∀[T:Type]. (Fan_d(T) ⇒ (∀A:(T List) ⟶ ℙ. (dbar(T;A) ⇒ (¬(down-closed(T;¬(A)) ∧ Unbounded(¬(A)))))))
BY
{ (Auto THEN (D 0 THENA Auto) THEN (With ⌜A⌝ (D 2)⋅ THENA Auto) THEN ThinTrivial THEN Auto) }

1
1. T : Type
2. A : (T List) ⟶ ℙ
3. dbar(T;A)
4. down-closed(T;¬(A))
5. Unbounded(¬(A))
6. ubar(T;A)
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type]
    (Fan\_d(T)  {}\mRightarrow{}  (\mforall{}A:(T  List)  {}\mrightarrow{}  \mBbbP{}.  (dbar(T;A)  {}\mRightarrow{}  (\mneg{}(down-closed(T;\mneg{}(A))  \mwedge{}  Unbounded(\mneg{}(A)))))))


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  (With  \mkleeneopen{}A\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)  THEN  ThinTrivial  THEN  Auto)

---

Home Index