---

Step * of Lemma induced-rmetric_wf

∀[Y:Type]. ∀[f:Y ⟶ ℝ].  (induced-rmetric(f) ∈ metric(Y))
BY
{ ((InstLemma `induced-metric_wf` [⌜ℝ⌝;⌜rmetric()⌝]⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast')) }

1
1. [Y] : Type
2. [f] : Y ⟶ ℝ
3. induced-metric(rmetric();f) ∈ metric(Y)
⊢ induced-rmetric(f) ∈ metric(Y)

---

Latex:

---

Latex:
\mforall{}[Y:Type].  \mforall{}[f:Y  {}\mrightarrow{}  \mBbbR{}].    (induced-rmetric(f)  \mmember{}  metric(Y))


By

---

Latex:
((InstLemma  `induced-metric\_wf`  [\mkleeneopen{}\mBbbR{}\mkleeneclose{};\mkleeneopen{}rmetric()\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast'))

---

Home Index