---

Step * 2 1 of Lemma rn-prod-metric-le-max-metric


1. n : ℤ
2. 0 < n
3. ∀x,y:ℝ^n - 1.  (Σ{|(x i) - y i| | 0≤i≤n - 1 - 1} ≤ (r(n - 1) * (max-metric(n - 1) x y)))
4. x : ℝ^n
5. y : ℝ^n
⊢ ((r(n - 1) * (max-metric(n - 1) x y)) + |(x (n - 1)) - y (n - 1)|) ≤ (r(n) * (max-metric(n) x y))
BY
{ Assert ⌜((max-metric(n - 1) x y) ≤ (max-metric(n) x y)) ∧ (|(x (n - 1)) - y (n - 1)| ≤ (max-metric(n) x y))⌝⋅ }

1
.....assertion..... 
1. n : ℤ
2. 0 < n
3. ∀x,y:ℝ^n - 1.  (Σ{|(x i) - y i| | 0≤i≤n - 1 - 1} ≤ (r(n - 1) * (max-metric(n - 1) x y)))
4. x : ℝ^n
5. y : ℝ^n
⊢ ((max-metric(n - 1) x y) ≤ (max-metric(n) x y)) ∧ (|(x (n - 1)) - y (n - 1)| ≤ (max-metric(n) x y))

2
1. n : ℤ
2. 0 < n
3. ∀x,y:ℝ^n - 1.  (Σ{|(x i) - y i| | 0≤i≤n - 1 - 1} ≤ (r(n - 1) * (max-metric(n - 1) x y)))
4. x : ℝ^n
5. y : ℝ^n
6. ((max-metric(n - 1) x y) ≤ (max-metric(n) x y)) ∧ (|(x (n - 1)) - y (n - 1)| ≤ (max-metric(n) x y))
⊢ ((r(n - 1) * (max-metric(n - 1) x y)) + |(x (n - 1)) - y (n - 1)|) ≤ (r(n) * (max-metric(n) x y))

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}x,y:\mBbbR{}\^{}n  -  1.    (\mSigma{}\{|(x  i)  -  y  i|  |  0\mleq{}i\mleq{}n  -  1  -  1\}  \mleq{}  (r(n  -  1)  *  (max-metric(n  -  1)  x  y)))
4.  x  :  \mBbbR{}\^{}n
5.  y  :  \mBbbR{}\^{}n
\mvdash{}  ((r(n  -  1)  *  (max-metric(n  -  1)  x  y))  +  |(x  (n  -  1))  -  y  (n  -  1)|)  \mleq{}  (r(n)  *  (max-metric(n)  x  y))


By

---

Latex:
Assert  \mkleeneopen{}((max-metric(n  -  1)  x  y)  \mleq{}  (max-metric(n)  x  y))
                \mwedge{}  (|(x  (n  -  1))  -  y  (n  -  1)|  \mleq{}  (max-metric(n)  x  y))\mkleeneclose{}\mcdot{}

---

Home Index