---

Step * 1 of Lemma real-vec-dist-lower-bound


1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. ∀v:ℝ^n. (||v|| = d(v;λi.r0))
⊢ |d(λi.r0;y) - d(λi.r0;x)| ≤ d(y;x)
BY
{ ((BLemma `rabs-difference-bound-rleq` THENA Auto)
   THEN (Assert d(y;x) = d(x;y) BY
               Auto)
   THEN (InstLemma `real-vec-triangle-inequality` [⌜n⌝;⌜λi.r0⌝;⌜y⌝;⌜x⌝]⋅ THENA Auto)
   THEN InstLemma `real-vec-triangle-inequality` [⌜n⌝;⌜λi.r0⌝;⌜x⌝;⌜y⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbR{}\^{}n
3.  y  :  \mBbbR{}\^{}n
4.  \mforall{}v:\mBbbR{}\^{}n.  (||v||  =  d(v;\mlambda{}i.r0))
\mvdash{}  |d(\mlambda{}i.r0;y)  -  d(\mlambda{}i.r0;x)|  \mleq{}  d(y;x)


By

---

Latex:
((BLemma  `rabs-difference-bound-rleq`  THENA  Auto)
  THEN  (Assert  d(y;x)  =  d(x;y)  BY
                          Auto)
  THEN  (InstLemma  `real-vec-triangle-inequality`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}i.r0\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstLemma  `real-vec-triangle-inequality`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}i.r0\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index