---

Step * of Lemma meq-max-metric

∀[n:ℕ]. ∀[x,y:ℝ^n].  uiff(x ≡ y;req-vec(n;x;y))
BY
{ (Intros THEN (RWO "meq-max-metric-iff-meq-rn-metric" 0 THENA Auto) 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  (RWO  "meq-max-metric-iff-meq-rn-metric"  0  THENA  Auto)  THEN  EAuto  1)

---

Home Index