---

Step * of Lemma rn-prod-metric_wf

∀[n:ℕ]. (rn-prod-metric(n) ∈ metric(ℝ^n))
BY
{ (Unfold `real-vec` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (rn-prod-metric(n)  \mmember{}  metric(\mBbbR{}\^{}n))


By

---

Latex:
(Unfold  `real-vec`  0  THEN  ProveWfLemma)

---

Home Index