---

Step * 2 of Lemma es-increasing-sequence2


1. es : EO@i'
2. m : ℕ+@i
3. f : ℕm ─→ E@i
4. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
5. i : ℕm@i
6. j : ℕi + 1@i
7. ∀i:ℕm. ∀j:ℕi.  (f j <loc f i)
8. ¬(i = j ∈ ℤ)
⊢ f j ≤loc f i 
BY
{ (Unfold `es-le` 0 THEN OrLeft THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  m  :  \mBbbN{}\msupplus{}@i
3.  f  :  \mBbbN{}m  {}\mrightarrow{}  E@i
4.  \mforall{}i:\mBbbN{}m  -  1.  (f  i  <loc  f  (i  +  1))@i
5.  i  :  \mBbbN{}m@i
6.  j  :  \mBbbN{}i  +  1@i
7.  \mforall{}i:\mBbbN{}m.  \mforall{}j:\mBbbN{}i.    (f  j  <loc  f  i)
8.  \mneg{}(i  =  j)
\mvdash{}  f  j  \mleq{}loc  f  i 


By

(Unfold  `es-le`  0  THEN  OrLeft  THEN  Auto)

---

Home Index