---

Step * of Lemma real-vec-norm-diff-bound

∀[n:ℕ]. ∀[x,y:ℝ^n].  (|||x|| - ||y||| ≤ d(x;y))
BY
{ (Auto
   THEN (InstLemma `real-vec-triangle-inequality` [⌜n⌝;⌜x⌝;⌜y⌝;⌜λi.r0⌝]⋅ THENA Auto)
   THEN (RWO "real-vec-dist-from-zero" (-1)⋅ THENA Auto)
   THEN (InstLemma `real-vec-triangle-inequality` [⌜n⌝;⌜y⌝;⌜x⌝;⌜λi.r0⌝]⋅ THENA Auto)
   THEN (RWO "real-vec-dist-from-zero" (-1)⋅ THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. ||x|| ≤ (d(x;y) + ||y||)
5. ||y|| ≤ (d(y;x) + ||x||)
⊢ |||x|| - ||y||| ≤ d(x;y)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    (|||x||  -  ||y|||  \mleq{}  d(x;y))


By

---

Latex:
(Auto
  THEN  (InstLemma  `real-vec-triangle-inequality`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}\mlambda{}i.r0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "real-vec-dist-from-zero"  (-1)\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `real-vec-triangle-inequality`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}i.r0\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "real-vec-dist-from-zero"  (-1)\mcdot{}  THENA  Auto))

---

Home Index