---

Step * of Lemma real-vec-sep-iff-dot-product

∀n:ℕ. ∀x,y:ℝ^n.  (x ≠ y ⇐⇒ r0 < y - x⋅y - x)
BY
{ (Intros THEN (RWO "real-vec-sep-0-iff<" 0 THENA Auto) THEN (RWO "real-vec-sep-iff" 0 THENA Auto)) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
⊢ ∃i:ℕn. (r0 < |(x i) - y i|) ⇐⇒ ∃i:ℕn. (r0 < |(y - x i) - (λi.r0) i|)

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}\^{}n.    (x  \mneq{}  y  \mLeftarrow{}{}\mRightarrow{}  r0  <  y  -  x\mcdot{}y  -  x)


By

---

Latex:
(Intros  THEN  (RWO  "real-vec-sep-0-iff<"  0  THENA  Auto)  THEN  (RWO  "real-vec-sep-iff"  0  THENA  Auto))

---

Home Index