---

Step * 1 of Lemma frs-mesh-bound


1. p : ℝ List
2. ¬||p|| < 2
3. x : ℝ
4. r0 ≤ x
5. ∀[i:ℕ||p|| - 1]. ((p[i + 1] - p[i]) ≤ x)
⊢ rmaximum(0;||p|| - 2;i.p[i + 1] - p[i]) ≤ x
BY
{ (BLemma `rmaximum-lub` THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  \mBbbR{}  List
2.  \mneg{}||p||  <  2
3.  x  :  \mBbbR{}
4.  r0  \mleq{}  x
5.  \mforall{}[i:\mBbbN{}||p||  -  1].  ((p[i  +  1]  -  p[i])  \mleq{}  x)
\mvdash{}  rmaximum(0;||p||  -  2;i.p[i  +  1]  -  p[i])  \mleq{}  x


By

---

Latex:
(BLemma  `rmaximum-lub`  THEN  Auto)

---

Home Index