---

Step * of Lemma nearby-frs-mesh

No Annotations
∀e:{e:ℝ| r0 < e} . ∀p,q:ℝ List.  (nearby-partitions(e;q;p) ⇒ (frs-mesh(p) ≤ (frs-mesh(q) + (r(2) * e))))
BY
{ (Auto THEN Unfold `frs-mesh` 0 THEN D -1 THEN (Subst' ||q|| ~ ||p|| 0 THENA Auto) THEN AutoSplit) }

1
1. e : {e:ℝ| r0 < e} 
2. p : ℝ List
3. ¬||p|| < 2
4. q : ℝ List
5. ||q|| = ||p|| ∈ ℤ
6. ∀i:ℕ||q||. (|q[i] - p[i]| ≤ e)
⊢ rmaximum(0;||p|| - 2;i.p[i + 1] - p[i]) ≤ (rmaximum(0;||p|| - 2;i.q[i + 1] - q[i]) + (r(2) * e))

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:\{e:\mBbbR{}|  r0  <  e\}  .  \mforall{}p,q:\mBbbR{}  List.
    (nearby-partitions(e;q;p)  {}\mRightarrow{}  (frs-mesh(p)  \mleq{}  (frs-mesh(q)  +  (r(2)  *  e))))


By

---

Latex:
(Auto  THEN  Unfold  `frs-mesh`  0  THEN  D  -1  THEN  (Subst'  ||q||  \msim{}  ||p||  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index