Step
*
1
1
1
1
of Lemma
rabs-difference-rmax
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. y : ℝ
5. n : ℕ+@i
6. m : {1...}@i
⊢ ((-2) * m) ≤ (n * (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|)))
BY
{ Assert ⌜0 ≤ (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|))⌝⋅ }
1
.....assertion.....
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. y : ℝ
5. n : ℕ+@i
6. m : {1...}@i
⊢ 0 ≤ (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|))
2
1. a : ℝ
2. b : ℝ
3. x : ℝ
4. y : ℝ
5. n : ℕ+@i
6. m : {1...}@i
7. 0 ≤ (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|))
⊢ ((-2) * m) ≤ (n * (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|)))
Latex:
Latex:
1. a : \mBbbR{}
2. b : \mBbbR{}
3. x : \mBbbR{}
4. y : \mBbbR{}
5. n : \mBbbN{}\msupplus{}@i
6. m : \{1...\}@i
\mvdash{} ((-2) * m) \mleq{} (n
* (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|)))
By
Latex:
Assert \mkleeneopen{}0 \mleq{} (imax(|(x m) + (-(a m))|;|(y m) + (-(b m))|) + (-|imax(x m;y m) + (-imax(a m;b m))|))\mkleeneclose{}\mcdot{}
Home
Index