Step
*
1
2
of Lemma
derivative-id
1. I : Interval
2. k : ℕ+@i
3. n : {n:ℕ+| icompact(i-approx(I;n))} @i
4. r0 < r(100)
5. x : ℝ@i
6. y : ℝ@i
7. x ∈ i-approx(I;n)@i
8. y ∈ i-approx(I;n)@i
9. |y - x| ≤ r(100)@i
10. |y - x - r1 * (y - x)| = r0
⊢ |y - x - r1 * (y - x)| ≤ ((r1/r(k)) * |y - x|)
BY
{ (RWO "-1" 0 THEN Auto) }
Latex:
Latex:
1. I : Interval
2. k : \mBbbN{}\msupplus{}@i
3. n : \{n:\mBbbN{}\msupplus{}| icompact(i-approx(I;n))\} @i
4. r0 < r(100)
5. x : \mBbbR{}@i
6. y : \mBbbR{}@i
7. x \mmember{} i-approx(I;n)@i
8. y \mmember{} i-approx(I;n)@i
9. |y - x| \mleq{} r(100)@i
10. |y - x - r1 * (y - x)| = r0
\mvdash{} |y - x - r1 * (y - x)| \mleq{} ((r1/r(k)) * |y - x|)
By
Latex:
(RWO "-1" 0 THEN Auto)
Home
Index