Step
*
1
of Lemma
real-vec-sep-implies
1. n : ℕ
2. a : ℝ^n
3. c : ℝ^n
4. r0 < d(a;c)
5. r0 < d(a;c)^2
⊢ ∃i:ℕn. (r0 < |(a i) - c i|)
BY
{ RepUR ``real-vec-dist real-vec-norm`` -1 }
1
1. n : ℕ
2. a : ℝ^n
3. c : ℝ^n
4. r0 < d(a;c)
5. r0 < rsqrt(a - c⋅a - c)^2
⊢ ∃i:ℕn. (r0 < |(a i) - c i|)
Latex:
Latex:
1. n : \mBbbN{}
2. a : \mBbbR{}\^{}n
3. c : \mBbbR{}\^{}n
4. r0 < d(a;c)
5. r0 < d(a;c)\^{}2
\mvdash{} \mexists{}i:\mBbbN{}n. (r0 < |(a i) - c i|)
By
Latex:
RepUR ``real-vec-dist real-vec-norm`` -1
Home
Index