---

Step * 2 1 1 of Lemma rv-between-simple


1. n : ℕ
2. c : ℝ^n
3. d : ℝ^n
4. r0 < ||d||
5. c - d-c-c + d
6. d(c - d;c + d) = (d(c - d;c) + d(c;c + d))
⊢ c - d ≠ c + d
BY
{ (UnfoldTopAb 0
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO "real-vec-dist-symmetry" 0 THENA Auto)
   THEN Unfold `real-vec-dist` 0) }

1
1. n : ℕ
2. c : ℝ^n
3. d : ℝ^n
4. r0 < ||d||
5. c - d-c-c + d
6. d(c - d;c + d) = (d(c - d;c) + d(c;c + d))
⊢ r0 < (||c - c - d|| + ||c + d - c||)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  c  :  \mBbbR{}\^{}n
3.  d  :  \mBbbR{}\^{}n
4.  r0  <  ||d||
5.  c  -  d-c-c  +  d
6.  d(c  -  d;c  +  d)  =  (d(c  -  d;c)  +  d(c;c  +  d))
\mvdash{}  c  -  d  \mneq{}  c  +  d


By

---

Latex:
(UnfoldTopAb  0
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "real-vec-dist-symmetry"  0  THENA  Auto)
  THEN  Unfold  `real-vec-dist`  0)

---

Home Index