---

Step * 2 of Lemma metric-symmetry


1. X : Type
2. d : X ⟶ X ⟶ ℝ
3. ∀x,y,z:X.  ((d x z) ≤ ((d x y) + (d z y)))
4. ∀x:X. ((d x x) = r0)
5. x : X
6. y : X
7. (d y x) ≤ (r0 + (d x y))
8. (d x y) ≤ (r0 + (d y x))
⊢ (d y x) ≤ (d x y)
BY
{ (RWO "-2" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  X  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbR{}
3.  \mforall{}x,y,z:X.    ((d  x  z)  \mleq{}  ((d  x  y)  +  (d  z  y)))
4.  \mforall{}x:X.  ((d  x  x)  =  r0)
5.  x  :  X
6.  y  :  X
7.  (d  y  x)  \mleq{}  (r0  +  (d  x  y))
8.  (d  x  y)  \mleq{}  (r0  +  (d  y  x))
\mvdash{}  (d  y  x)  \mleq{}  (d  x  y)


By

---

Latex:
(RWO  "-2"  0  THEN  Auto)

---

Home Index