Step
*
1
of Lemma
real-vec-triangle-inequality
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. z : ℝ^n
⊢ ||x - z|| ≤ ||x - y + y - z||
BY
{ (Assert ||x - y + y - z|| = ||x - z|| BY
(BLemma `real-vec-norm_functionality`
THEN Auto
THEN D 0
THEN Auto
THEN RepUR ``real-vec-sub real-vec-add`` 0
THEN nRNorm 0
THEN Auto)) }
1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. z : ℝ^n
5. ||x - y + y - z|| = ||x - z||
⊢ ||x - z|| ≤ ||x - y + y - z||
Latex:
Latex:
1. n : \mBbbN{}
2. x : \mBbbR{}\^{}n
3. y : \mBbbR{}\^{}n
4. z : \mBbbR{}\^{}n
\mvdash{} ||x - z|| \mleq{} ||x - y + y - z||
By
Latex:
(Assert ||x - y + y - z|| = ||x - z|| BY
(BLemma `real-vec-norm\_functionality`
THEN Auto
THEN D 0
THEN Auto
THEN RepUR ``real-vec-sub real-vec-add`` 0
THEN nRNorm 0
THEN Auto))
Home
Index