Step
*
2
of Lemma
real-vec-sep-msep-prod-metric
1. n : ℕ
2. a : ℝ^n
3. c : ℝ^n
4. r0 < Σ{|(a i) - c i| | 0≤i≤n - 1}
⊢ ∃i:ℕn. (r0 < |(a i) - c i|)
BY
{ (RWO "rsum-of-nonneg-positive-iff" (-1) THEN Auto THEN ParallelLast) }
Latex:
Latex:
1. n : \mBbbN{}
2. a : \mBbbR{}\^{}n
3. c : \mBbbR{}\^{}n
4. r0 < \mSigma{}\{|(a i) - c i| | 0\mleq{}i\mleq{}n - 1\}
\mvdash{} \mexists{}i:\mBbbN{}n. (r0 < |(a i) - c i|)
By
Latex:
(RWO "rsum-of-nonneg-positive-iff" (-1) THEN Auto THEN ParallelLast)
Home
Index