---

Step * of Lemma real-vec-sep-iff-rneq

∀n:ℕ. ∀a,c:ℝ^n.  (a ≠ c ⇐⇒ ∃i:ℕn. a i ≠ c i)
BY
{ ((UnivCD THENA Auto) THEN (RWO "real-vec-sep-iff" 0 THENA Auto) THEN RWO "rneq-iff-rabs<" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a,c:\mBbbR{}\^{}n.    (a  \mneq{}  c  \mLeftarrow{}{}\mRightarrow{}  \mexists{}i:\mBbbN{}n.  a  i  \mneq{}  c  i)


By

---

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

---

Home Index