---

Step * 2 1 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
6. v : ℝ
7. (max-metric(n - 1) x y) = v ∈ ℝ
8. v1 : ℝ
9. (max-metric(n) x y) = v1 ∈ ℝ
10. v2 : ℝ
11. |(x (n - 1)) - y (n - 1)| = v2 ∈ ℝ
⊢ ((v ≤ v1) ∧ (v2 ≤ v1)) ⇒ (((r(n - 1) * v) + v2) ≤ (r(n) * v1))
BY
{ ((Assert r(n) = (r(n - 1) + r1) BY
          (RWO "radd-int" 0 THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN (GenConcl ⌜r(n - 1) = c ∈ {c:ℝ| r0 ≤ c} ⌝⋅ THENA Auto)) }

1
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. v : ℝ
7. (max-metric(n - 1) x y) = v ∈ ℝ
8. v1 : ℝ
9. (max-metric(n) x y) = v1 ∈ ℝ
10. v2 : ℝ
11. |(x (n - 1)) - y (n - 1)| = v2 ∈ ℝ
12. r(n) = (r(n - 1) + r1)
13. c : {c:ℝ| r0 ≤ c} 
14. r(n - 1) = c ∈ {c:ℝ| r0 ≤ c} 
⊢ ((v ≤ v1) ∧ (v2 ≤ v1)) ⇒ (((c * v) + v2) ≤ ((c + r1) * v1))

---

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
6.  v  :  \mBbbR{}
7.  (max-metric(n  -  1)  x  y)  =  v
8.  v1  :  \mBbbR{}
9.  (max-metric(n)  x  y)  =  v1
10.  v2  :  \mBbbR{}
11.  |(x  (n  -  1))  -  y  (n  -  1)|  =  v2
\mvdash{}  ((v  \mleq{}  v1)  \mwedge{}  (v2  \mleq{}  v1))  {}\mRightarrow{}  (((r(n  -  1)  *  v)  +  v2)  \mleq{}  (r(n)  *  v1))


By

---

Latex:
((Assert  r(n)  =  (r(n  -  1)  +  r1)  BY
                (RWO  "radd-int"  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}r(n  -  1)  =  c\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index