---

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

No Annotations
∀[n:ℕ]. ∀[x,y:ℝ^n].  (|||y|| - ||x||| ≤ d(x;y))
BY
{ (Auto
   THEN (Assert ∀v:ℝ^n. (||v|| = d(v;λi.r0)) BY
               ((D 0 THENA Auto)
                THEN Unfold `real-vec-dist` 0
                THEN BLemma `real-vec-norm_functionality`⋅
                THEN Auto
                THEN D 0
                THEN RepUR ``real-vec-sub`` 0
                THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO "real-vec-dist-symmetry" 0 THENA Auto)) }

1
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)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}v:\mBbbR{}\^{}n.  (||v||  =  d(v;\mlambda{}i.r0))  BY
                          ((D  0  THENA  Auto)
                            THEN  Unfold  `real-vec-dist`  0
                            THEN  BLemma  `real-vec-norm\_functionality`\mcdot{}
                            THEN  Auto
                            THEN  D  0
                            THEN  RepUR  ``real-vec-sub``  0
                            THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "real-vec-dist-symmetry"  0  THENA  Auto))

---

Home Index