Step
*
of Lemma
real-vec-sep-implies
No Annotations
∀n:ℕ. ∀a,c:ℝ^n. (a ≠ c
⇒ (∃i:ℕn. (r0 < |(a i) - c i|)))
BY
{ (Auto THEN Unfold `real-vec-sep` -1 THEN (Assert r0 < d(a;c)^2 BY (BLemma `rnexp-positive` THEN Auto))) }
1
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|)
Latex:
Latex:
No Annotations
\mforall{}n:\mBbbN{}. \mforall{}a,c:\mBbbR{}\^{}n. (a \mneq{} c {}\mRightarrow{} (\mexists{}i:\mBbbN{}n. (r0 < |(a i) - c i|)))
By
Latex:
(Auto
THEN Unfold `real-vec-sep` -1
THEN (Assert r0 < d(a;c)\^{}2 BY
(BLemma `rnexp-positive` THEN Auto)))
Home
Index