---

Step * of Lemma rn-metric_wf

∀[n:ℕ]. (rn-metric(n) ∈ metric(ℝ^n))
BY
{ (Auto
   THEN (Assert rn-metric(n) ∈ ℝ^n ⟶ ℝ^n ⟶ ℝ BY
               ProveWfLemma)
   THEN MemTypeCD
   THEN Auto
   THEN All (RepUR ``rn-metric``)
   THEN Auto
   THEN Try ((RWO "-1 -2" 0 THEN Auto THEN nRNorm 0 THEN Auto))) }

1
1. n : ℕ
2. λx,y. d(x;y) ∈ ℝ^n ⟶ ℝ^n ⟶ ℝ
3. ∀x,y:ℝ^n.  (r0 ≤ d(x;y))
4. x : ℝ^n
5. y : ℝ^n
6. z : ℝ^n
⊢ d(x;z) ≤ (d(x;y) + d(z;y))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Assert  rn-metric(n)  \mmember{}  \mBbbR{}\^{}n  {}\mrightarrow{}  \mBbbR{}\^{}n  {}\mrightarrow{}  \mBbbR{}  BY
                          ProveWfLemma)
  THEN  MemTypeCD
  THEN  Auto
  THEN  All  (RepUR  ``rn-metric``)
  THEN  Auto
  THEN  Try  ((RWO  "-1  -2"  0  THEN  Auto  THEN  nRNorm  0  THEN  Auto)))

---

Home Index