---

Step * of Lemma rn-metric-meq

∀[n:ℕ]. ∀[x,y:ℝ^n].  uiff(x ≡ y;req-vec(n;x;y))
BY
{ ((Intros THEN RepUR ``meq rn-metric`` 0) THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x,y:\mBbbR{}\^{}n].    uiff(x  \mequiv{}  y;req-vec(n;x;y))


By

---

Latex:
((Intros  THEN  RepUR  ``meq  rn-metric``  0)  THEN  EAuto  1)

---

Home Index