---

Step * of Lemma find-ge_wf

∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].  find-ge(f;n) ∈ {n':ℤ| (n ≤ n') ∧ f n' = tt}  supposing ∃m:{n...}. ∀k:{m...}. f k = tt
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[f:\{n...\}  {}\mrightarrow{}  \mBbbB{}].    find-ge(f;n)  \mmember{}  \{n':\mBbbZ{}|  (n  \mleq{}  n')  \mwedge{}  f  n'  =  tt\}    supposing  \mexists{}m:\{n...\}.  \mforall{}k:\{m..\000C.\}.  f  k  =  tt


By

---

Latex:
ProveWfLemma

---

Home Index