---

Step * of Lemma real-vec-dist-between

∀n:ℕ. ∀a,b,c:ℝ^n.  (a-b-c ⇒ (d(a;c) = (d(a;b) + d(b;c))))
BY
{ (Auto
   THEN RepeatFor 2 (D -1)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO "real-vec-dist-between-1 real-vec-dist-between-2" 0 THENA Auto)) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. t : ℝ
6. t ∈ (r0, r1)
7. req-vec(n;b;t*a + r1 - t*c)
⊢ d(a;c) = ((|r1 - t| * d(a;c)) + (|t| * d(a;c)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,b,c:\mBbbR{}\^{}n.    (a-b-c  {}\mRightarrow{}  (d(a;c)  =  (d(a;b)  +  d(b;c))))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -1)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "real-vec-dist-between-1  real-vec-dist-between-2"  0  THENA  Auto))

---

Home Index