---

Step * of Lemma frs-mesh-bound

∀[p:ℝ List]. ∀[x:ℝ].  ((r0 ≤ x) ⇒ (∀[i:ℕ||p|| - 1]. ((p[i + 1] - p[i]) ≤ x)) ⇒ (frs-mesh(p) ≤ x))
BY
{ (Auto THEN Unfold `frs-mesh` 0 THEN AutoSplit) }

1
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

---

Latex:

---

Latex:
\mforall{}[p:\mBbbR{}  List].  \mforall{}[x:\mBbbR{}].    ((r0  \mleq{}  x)  {}\mRightarrow{}  (\mforall{}[i:\mBbbN{}||p||  -  1].  ((p[i  +  1]  -  p[i])  \mleq{}  x))  {}\mRightarrow{}  (frs-mesh(p)  \mleq{}  x))


By

---

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

---

Home Index