---

Step * of Lemma real-subset-metric_wf

∀[P:ℝ ⟶ ℙ]. (real-subset-metric() ∈ metric(x:ℝ × P[x]))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbR{}  {}\mrightarrow{}  \mBbbP{}].  (real-subset-metric()  \mmember{}  metric(x:\mBbbR{}  \mtimes{}  P[x]))


By

---

Latex:
ProveWfLemma

---

Home Index