---

Step * of Lemma frs-mesh-nonneg

∀[p:ℝ List]. (frs-non-dec(p) ⇒ (r0 ≤ frs-mesh(p)))
BY
{ (Unfold `frs-mesh` 0 THEN Auto THEN AutoSplit THEN Try ((RelRST THEN Auto))) }

1
1. p : ℝ List
2. ¬||p|| < 2
3. frs-non-dec(p)
⊢ r0 ≤ rmaximum(0;||p|| - 2;i.p[i + 1] - p[i])

---

Latex:

---

Latex:
\mforall{}[p:\mBbbR{}  List].  (frs-non-dec(p)  {}\mRightarrow{}  (r0  \mleq{}  frs-mesh(p)))


By

---

Latex:
(Unfold  `frs-mesh`  0  THEN  Auto  THEN  AutoSplit  THEN  Try  ((RelRST  THEN  Auto)))

---

Home Index