---

Step * 1 1 of Lemma frs-mesh-nonneg


1. p : ℝ List
2. ¬||p|| < 2
3. frs-non-dec(p)
4. ∀[n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ].  (x[0] ≤ rmaximum(n;m;i.x[i])) supposing ((0 ≤ m) and (n ≤ 0))
⊢ r0 ≤ (p[0 + 1] - p[0])
BY
{ (nRAdd ⌜p[0]⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbR{}  List
2.  \mneg{}||p||  <  2
3.  frs-non-dec(p)
4.  \mforall{}[n,m:\mBbbZ{}].  \mforall{}[x:\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}].    (x[0]  \mleq{}  rmaximum(n;m;i.x[i]))  supposing  ((0  \mleq{}  m)  and  (n  \mleq{}  0))
\mvdash{}  r0  \mleq{}  (p[0  +  1]  -  p[0])


By

---

Latex:
(nRAdd  \mkleeneopen{}p[0]\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index