Step
*
1
1
1
1
1
1
of Lemma
rabs-difference-rmax
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. y : ℝ
5. n : ℕ+@i
6. m : {1...}@i
7. |imax(x m;y m) - imax(a m;b m)| ≤ imax(|(x m) - a m|;|(y m) - b m|)
⊢ 0 ≤ (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|))
BY
{ (All (RW IntNormC) THEN Auto) }
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. x : \mBbbR{}
4. y : \mBbbR{}
5. n : \mBbbN{}\msupplus{}@i
6. m : \{1...\}@i
7. |imax(x m;y m) - imax(a m;b m)| \mleq{} imax(|(x m) - a m|;|(y m) - b m|)
\mvdash{} 0 \mleq{} (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|))
By
Latex:
(All (RW IntNormC) THEN Auto)
Home
Index