---

Step * of Lemma es-increasing-sequence

∀es:EO. ∀m:ℕ+. ∀f:ℕm ─→ E.  ((∀i:ℕm - 1. (f i <loc f (i + 1))) ⇒ (∀i:ℕm. ∀j:ℕi.  (f j <loc f i)))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)))⋅ }

1
1. es : EO@i'
2. m : ℕ+@i
3. f : ℕm ─→ E@i
4. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
⊢ ∀i:ℕm. ∀j:ℕi.  (f j <loc f i)

---

Latex:


\mforall{}es:EO.  \mforall{}m:\mBbbN{}\msupplus{}.  \mforall{}f:\mBbbN{}m  {}\mrightarrow{}  E.    ((\mforall{}i:\mBbbN{}m  -  1.  (f  i  <loc  f  (i  +  1)))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}m.  \mforall{}j:\mBbbN{}i.    (f  j  <loc  f  i)))


By

(RepeatFor  4  ((D  0  THENA  Auto)))\mcdot{}

---

Home Index