---

Step * of Lemma rv-be-dist

∀[n:ℕ]. ∀[a,b,c:ℝ^n].  (a_b_c ⇒ (d(a;c) = (d(a;b) + d(b;c))))
BY
{ (Auto THEN BLemma `rv-T-dist` THEN Auto) }

1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. a_b_c
⊢ rv-T(n;a;b;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  BLemma  `rv-T-dist`  THEN  Auto)

---

Home Index