---

Step * 1 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. k : ℕ
6. ∀f:ℕ ⟶ T. ∃n:ℕk. (A map(f;upto(n)))
7. as : T List
8. ||as|| = (k + 1) ∈ ℤ
9. ¬(A) as
⊢ False
BY
{ ((With ⌜λi.if i <z k then as[i] else as[0] fi ⌝ (D (-4))⋅ THENA Auto) THEN D -1)⋅ }

1
1. T : Type
2. A : (T List) ⟶ ℙ
3. dbar(T;A)
4. down-closed(T;¬(A))
5. k : ℕ
6. as : T List
7. ||as|| = (k + 1) ∈ ℤ
8. ¬(A) as
9. n : ℕk
10. A map(λi.if i <z k then as[i] else as[0] fi ;upto(n))
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  (T  List)  {}\mrightarrow{}  \mBbbP{}
3.  dbar(T;A)
4.  down-closed(T;\mneg{}(A))
5.  k  :  \mBbbN{}
6.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  T.  \mexists{}n:\mBbbN{}k.  (A  map(f;upto(n)))
7.  as  :  T  List
8.  ||as||  =  (k  +  1)
9.  \mneg{}(A)  as
\mvdash{}  False


By

---

Latex:
((With  \mkleeneopen{}\mlambda{}i.if  i  <z  k  then  as[i]  else  as[0]  fi  \mkleeneclose{}  (D  (-4))\mcdot{}  THENA  Auto)  THEN  D  -1)\mcdot{}

---

Home Index