---

Step * 1 of Lemma induced-rmetric_wf


1. [Y] : Type
2. [f] : Y ⟶ ℝ
3. induced-metric(rmetric();f) ∈ metric(Y)
⊢ induced-rmetric(f) ∈ metric(Y)
BY
{ ((NthHypSq (-1) THEN Auto) THEN Computation) }

---

Latex:

---

Latex:

1.  [Y]  :  Type
2.  [f]  :  Y  {}\mrightarrow{}  \mBbbR{}
3.  induced-metric(rmetric();f)  \mmember{}  metric(Y)
\mvdash{}  induced-rmetric(f)  \mmember{}  metric(Y)


By

---

Latex:
((NthHypSq  (-1)  THEN  Auto)  THEN  Computation)

---

Home Index