---

Step * of Lemma fan_theorem-ext

∀[X:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ]
  (∀n:ℕ. ∀s:ℕn ⟶ 𝔹.  Dec(X[n;s])) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f]) supposing ∀f:ℕ ⟶ 𝔹. (↓∃n:ℕ. X[n;f])
BY
{ Extract of Obid: fan_theorem
  not unfolding  FAN int_seg_decide outl
  finishing with Auto
  normalizes to:
  
  λd.eval K = FAN(d) in
     <K, λf.outl(int_seg_decide(λn.(d n f);0;K))> }

---

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:
Extract  of  Obid:  fan\_theorem
not  unfolding    FAN  int\_seg\_decide  outl
finishing  with  Auto
normalizes  to:

\mlambda{}d.eval  K  =  FAN(d)  in
      <K,  \mlambda{}f.outl(int\_seg\_decide(\mlambda{}n.(d  n  f);0;K))>

---

Home Index