---

Step * of Lemma fan-realizer_test

∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. ((λl.(3 ≤ ||l||)) map(f;upto(n)))
BY
{ (InstLemma `fan-realizer_wf` []⋅ THEN Auto) }

1
1. fan-realizer ∈ ∀[X:(𝔹 List) ⟶ ℙ]. (tbar(𝔹;X) ⇒ Decidable(X) ⇒ (∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. (X map(f;upto(n)))))
⊢ ∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. ((λl.(3 ≤ ||l||)) map(f;upto(n)))

---

Latex:

---

Latex:
\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  ((\mlambda{}l.(3  \mleq{}  ||l||))  map(f;upto(n)))


By

---

Latex:
(InstLemma  `fan-realizer\_wf`  []\mcdot{}  THEN  Auto)

---

Home Index