---

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


1. T : Type
2. A : (T List) ⟶ ℙ
3. dbar(T;A)
4. down-closed(T;¬(A))
5. Unbounded(¬(A))
6. ubar(T;A)
⊢ False
BY
{ (D -1 THEN (D -3 With ⌜k + 1⌝  THENA Auto) THEN ExRepD) }

1
1. T : Type
2. A : (T List) ⟶ ℙ
3. dbar(T;A)
4. down-closed(T;¬(A))
5. k : ℕ
6. ∀f:ℕ ⟶ T. ∃n:ℕk. (A map(f;upto(n)))
7. as : T List
8. ||as|| = (k + 1) ∈ ℤ
9. ¬(A) as
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  dbar(T;A)
4.  down-closed(T;\mneg{}(A))
5.  Unbounded(\mneg{}(A))
6.  ubar(T;A)
\mvdash{}  False


By

---

Latex:
(D  -1  THEN  (D  -3  With  \mkleeneopen{}k  +  1\mkleeneclose{}    THENA  Auto)  THEN  ExRepD)

---

Home Index