---

Step * of Lemma adjacent-frs-points

∀[p:ℝ List]. ∀[i:ℕ||p|| - 1].  (frs-non-dec(p) ⇒ r0≤p[i + 1] - p[i]≤frs-mesh(p))
BY
{ (Auto THEN D 0) }

1
1. p : ℝ List
2. i : ℕ||p|| - 1
3. frs-non-dec(p)
⊢ r0 ≤ (p[i + 1] - p[i])

2
1. p : ℝ List
2. i : ℕ||p|| - 1
3. frs-non-dec(p)
⊢ (p[i + 1] - p[i]) ≤ frs-mesh(p)

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  D  0)

---

Home Index