---

Step * of Lemma mu-ge-property

∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].  {(↑(f mu-ge(f;n))) ∧ (∀[i:{n..mu-ge(f;n)-}]. (¬↑(f i)))} supposing ∃m:{n...}. (↑(f m))
BY
{ TACTIC:Auto }

1
1. n : ℤ
2. f : {n...} ⟶ 𝔹
3. ∃m:{n...}. (↑(f m))
⊢ {(↑(f mu-ge(f;n))) ∧ (∀[i:{n..mu-ge(f;n)-}]. (¬↑(f i)))}

---

Latex:

---

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


By

---

Latex:
TACTIC:Auto

---

Home Index