---

Step * of Lemma mu-ge_wf2

∀[n:ℤ]. ∀[f:{n...} ⟶ (Top + Top)].  mu-ge(f;n) ∈ {n...} supposing ∃m:{n...}. (↑isl(f m))
BY
{ ((UnivCD THENA Auto) THEN ExRepD THEN Assert ⌜∀d:ℕ. ((n ≤ (m - d)) ⇒ (mu-ge(f;m - d) ∈ {n...}))⌝⋅) }

1
.....assertion..... 
1. n : ℤ
2. f : {n...} ⟶ (Top + Top)
3. m : {n...}
4. ↑isl(f m)
⊢ ∀d:ℕ. ((n ≤ (m - d)) ⇒ (mu-ge(f;m - d) ∈ {n...}))

2
1. n : ℤ
2. f : {n...} ⟶ (Top + Top)
3. m : {n...}
4. ↑isl(f m)
5. ∀d:ℕ. ((n ≤ (m - d)) ⇒ (mu-ge(f;m - d) ∈ {n...}))
⊢ mu-ge(f;n) ∈ {n...}

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  ExRepD  THEN  Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  ((n  \mleq{}  (m  -  d))  {}\mRightarrow{}  (mu-ge(f;m  -  d)  \mmember{}  \{n...\}))\mkleeneclose{}\mcdot{})

---

Home Index