---

Step * 2 of Lemma adjacent-frs-points


1. p : ℝ List
2. i : ℕ||p|| - 1
3. frs-non-dec(p)
⊢ (p[i + 1] - p[i]) ≤ frs-mesh(p)
BY
{ (Unfold `frs-mesh` 0 THEN AutoSplit)⋅ }

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

---

Latex:

---

Latex:

1.  p  :  \mBbbR{}  List
2.  i  :  \mBbbN{}||p||  -  1
3.  frs-non-dec(p)
\mvdash{}  (p[i  +  1]  -  p[i])  \mleq{}  frs-mesh(p)


By

---

Latex:
(Unfold  `frs-mesh`  0  THEN  AutoSplit)\mcdot{}

---

Home Index