---

Step * 1 1 1 1 of Lemma frs-non-dec-sum


1. u : ℝ
2. v : ℝ List
3. 1 < ||v|| + 1
4. ∀i,j:ℕ||[u / v]||.  ((i ≤ j) ⇒ ([u / v][i] ≤ [u / v][j]))
5. 1 < ||v||
6. i : ℕ||v||
7. j : ℕ||v||
8. i ≤ j
⊢ v[i] ≤ v[j]
BY
{ (InstHyp [⌜i + 1⌝;⌜j + 1⌝] 4⋅ THENA Auto) }

1
1. u : ℝ
2. v : ℝ List
3. 1 < ||v|| + 1
4. ∀i,j:ℕ||[u / v]||.  ((i ≤ j) ⇒ ([u / v][i] ≤ [u / v][j]))
5. 1 < ||v||
6. i : ℕ||v||
7. j : ℕ||v||
8. i ≤ j
9. [u / v][i + 1] ≤ [u / v][j + 1]
⊢ v[i] ≤ v[j]

---

Latex:

---

Latex:

1.  u  :  \mBbbR{}
2.  v  :  \mBbbR{}  List
3.  1  <  ||v||  +  1
4.  \mforall{}i,j:\mBbbN{}||[u  /  v]||.    ((i  \mleq{}  j)  {}\mRightarrow{}  ([u  /  v][i]  \mleq{}  [u  /  v][j]))
5.  1  <  ||v||
6.  i  :  \mBbbN{}||v||
7.  j  :  \mBbbN{}||v||
8.  i  \mleq{}  j
\mvdash{}  v[i]  \mleq{}  v[j]


By

---

Latex:
(InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{};\mkleeneopen{}j  +  1\mkleeneclose{}]  4\mcdot{}  THENA  Auto)

---

Home Index