---

Step * of Lemma mu-ge_wf

∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].  mu-ge(f;n) ∈ {n...} supposing ∃m:{n...}. (↑(f m))
BY
{ (InstLemma `mu-ge_wf2` [] THEN RepeatFor 4 (ParallelLast)) }

1
1. ∀[n:ℤ]. ∀[f:{n...} ⟶ (Top + Top)].  mu-ge(f;n) ∈ {n...} supposing ∃m:{n...}. (↑isl(f m))
2. n : ℤ
3. ∀[f:{n...} ⟶ (Top + Top)]. mu-ge(f;n) ∈ {n...} supposing ∃m:{n...}. (↑isl(f m))
4. f : {n...} ⟶ 𝔹
5. m : {n...}
6. ↑(f m)
⊢ ↑isl(f m)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbZ{}].  \mforall{}[f:\{n...\}  {}\mrightarrow{}  \mBbbB{}].    mu-ge(f;n)  \mmember{}  \{n...\}  supposing  \mexists{}m:\{n...\}.  (\muparrow{}(f  m))


By

---

Latex:
(InstLemma  `mu-ge\_wf2`  []  THEN  RepeatFor  4  (ParallelLast))

---

Home Index