---

Step * of Lemma fan_theorem

∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
BY
{ (InstLemma `simple_fan_theorem\'-ext` []
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN D -1
   THEN (Evaluate ⌜K = k ∈ ℤ⌝⋅ THENA Auto)
   THEN With ⌜K⌝ (D 0)⋅
   THEN Auto
   THEN (Assert ¬¬(∃n:ℕK. X[n;f]) BY
               ((D 0 THEN Auto) THEN D 5 With ⌜f⌝  THEN Auto THEN D -2 THEN ParallelLast))) }

1
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]

---

Latex:

---

Latex:
\mforall{}[X:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}]
    (\mforall{}n:\mBbbN{}.  \mforall{}s:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}.    Dec(X[n;s]))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f]) 
    supposing  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  (\mdownarrow{}\mexists{}n:\mBbbN{}.  X[n;f])


By

---

Latex:
(InstLemma  `simple\_fan\_theorem\mbackslash{}'-ext`  []
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  D  -1
  THEN  (Evaluate  \mkleeneopen{}K  =  k\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  With  \mkleeneopen{}K\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (Assert  \mneg{}\mneg{}(\mexists{}n:\mBbbN{}K.  X[n;f])  BY
                          ((D  0  THEN  Auto)  THEN  D  5  With  \mkleeneopen{}f\mkleeneclose{}    THEN  Auto  THEN  D  -2  THEN  ParallelLast)))

---

Home Index