Step
*
1
1
of Lemma
real-vec-sep-implies
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|)
BY
{ ((RWO "rnexp2" (-1) THENA Auto)
THEN (RWO "rsqrt_squared" (-1) THENA Auto)
THEN RepUR ``dot-product real-vec-sub`` -1) }
1
1. n : ℕ
2. a : ℝ^n
3. c : ℝ^n
4. r0 < d(a;c)
5. r0 < Σ{((a i) - c i) * ((a i) - c i) | 0≤i≤n - 1}
⊢ ∃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 < rsqrt(a - c\mcdot{}a - c)\^{}2
\mvdash{} \mexists{}i:\mBbbN{}n. (r0 < |(a i) - c i|)
By
Latex:
((RWO "rnexp2" (-1) THENA Auto)
THEN (RWO "rsqrt\_squared" (-1) THENA Auto)
THEN RepUR ``dot-product real-vec-sub`` -1)
Home
Index