Step * of Lemma real-vec-dist-between-2

n:ℕ. ∀a,c:ℝ^n. ∀t:ℝ.  (d(t*a r1 t*c;c) (|t| d(a;c)))
BY
Auto }

1
1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. : ℝ
⊢ d(t*a r1 t*c;c) (|t| d(a;c))


Latex:


Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,c:\mBbbR{}\^{}n.  \mforall{}t:\mBbbR{}.    (d(t*a  +  r1  -  t*c;c)  =  (|t|  *  d(a;c)))


By


Latex:
Auto




Home Index