---

Step * 1 of Lemma frs-mesh-nonneg


1. p : ℝ List
2. ¬||p|| < 2
3. frs-non-dec(p)
⊢ r0 ≤ rmaximum(0;||p|| - 2;i.p[i + 1] - p[i])
BY
{ (((InstLemma `rmaximum_ub` [⌜0⌝])⋅ THENA Auto) THEN RWO "-1<" 0 THEN Auto)⋅ }

1
1. p : ℝ List
2. ¬||p|| < 2
3. frs-non-dec(p)
4. ∀[n,m:ℤ]. ∀[x:{n..m + 1-} ⟶ ℝ].  (x[0] ≤ rmaximum(n;m;i.x[i])) supposing ((0 ≤ m) and (n ≤ 0))
⊢ r0 ≤ (p[0 + 1] - p[0])

---

Latex:

---

Latex:

1.  p  :  \mBbbR{}  List
2.  \mneg{}||p||  <  2
3.  frs-non-dec(p)
\mvdash{}  r0  \mleq{}  rmaximum(0;||p||  -  2;i.p[i  +  1]  -  p[i])


By

---

Latex:
(((InstLemma  `rmaximum\_ub`  [\mkleeneopen{}0\mkleeneclose{}])\mcdot{}  THENA  Auto)  THEN  RWO  "-1<"  0  THEN  Auto)\mcdot{}

---

Home Index