---

Step * 1 of Lemma fan_theorem


1. [X] : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ
2. ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
3. ∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])
4. k : ℕ
5. [%5] : ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]
6. K : ℤ
7. K = k ∈ ℤ
8. f : ℕ ⟶ 𝔹
9. ¬¬(∃n:ℕK. X[n;f])
⊢ ∃n:ℕK. X[n;f]
BY
{ (RenameVar `d' 3 THEN UseWitness ⌜outl(int_seg_decide(λn.(d n f);0;K))⌝⋅) }

1
1. X : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ
2. ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
3. d : ∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])
4. k : ℕ
5. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]
6. K : ℤ
7. K = k ∈ ℤ
8. f : ℕ ⟶ 𝔹
9. ¬¬(∃n:ℕK. X[n;f])
⊢ outl(int_seg_decide(λn.(d n f);0;K)) ∈ ∃n:ℕK. X[n;f]

---

Latex:

---

Latex:

1.  [X]  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])
3.  \mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    Dec(X[n;s])
4.  k  :  \mBbbN{}
5.  [\%5]  :  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f]
6.  K  :  \mBbbZ{}
7.  K  =  k
8.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
9.  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}K.  X[n;f])
\mvdash{}  \mexists{}n:\mBbbN{}K.  X[n;f]


By

---

Latex:
(RenameVar  `d'  3  THEN  UseWitness  \mkleeneopen{}outl(int\_seg\_decide(\mlambda{}n.(d  n  f);0;K))\mkleeneclose{}\mcdot{})

---

Home Index