---

Step * of Lemma simple-fan-theorem

∀[X:(𝔹 List) ⟶ ℙ]. ∀bar:tbar(𝔹;X). ∀d:Decidable(X).  (∃k:{ℕ| (∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n))))})
BY
{ (Auto THEN InstLemma `simple_fan_theorem` [⌜λ2n f.X map(f;upto(n))⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:(\mBbbB{}  List)  {}\mrightarrow{}  \mBbbP{}]
    \mforall{}bar:tbar(\mBbbB{};X).  \mforall{}d:Decidable(X).    (\mexists{}k:\{\mBbbN{}|  (\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  (X  map(f;upto(n))))\})


By

---

Latex:
(Auto  THEN  InstLemma  `simple\_fan\_theorem`  [\mkleeneopen{}\mlambda{}\msubtwo{}n  f.X  map(f;upto(n))\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index