---

Step * of Lemma rmetric_wf

rmetric() ∈ metric(ℝ)
BY
{ ((Assert rmetric() ∈ ℝ ⟶ ℝ ⟶ ℝ BY
          ProveWfLemma)
   THEN MemTypeCD
   THEN Auto
   THEN All (RepUR ``rmetric``)
   THEN Auto
   THEN Try ((RWO "-1 -2" 0 THEN Auto THEN nRNorm 0 THEN Auto))) }

1
1. λx,y. |x - y| ∈ ℝ ⟶ ℝ ⟶ ℝ
2. ∀x,y:ℝ.  (r0 ≤ |x - y|)
3. x : ℝ
4. y : ℝ
5. z : ℝ
⊢ |x - z| ≤ (|x - y| + |z - y|)

2
1. λx,y. |x - y| ∈ ℝ ⟶ ℝ ⟶ ℝ
2. ∀x,y:ℝ.  (r0 ≤ |x - y|)
3. ∀x,y,z:ℝ.  (|x - z| ≤ (|x - y| + |z - y|))
4. x : ℝ
⊢ |x - x| = r0

---

Latex:

---

Latex:
rmetric()  \mmember{}  metric(\mBbbR{})


By

---

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

---

Home Index