---

Step * of Lemma rn-metric-msep

No Annotations
∀n:ℕ. ∀x,y:ℝ^n.  (x # y ⇐⇒ x ≠ y)
BY
{ (Intros THEN Unfold `msep` 0 THEN (RWO  "rn-metric-sep" 0 THENA Auto) THEN RWO "real-vec-sep-iff-rneq" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}\^{}n.    (x  \#  y  \mLeftarrow{}{}\mRightarrow{}  x  \mneq{}  y)


By

---

Latex:
(Intros
  THEN  Unfold  `msep`  0
  THEN  (RWO    "rn-metric-sep"  0  THENA  Auto)
  THEN  RWO  "real-vec-sep-iff-rneq"  0
  THEN  Auto)

---

Home Index