---

Step * of Lemma metric-symmetry

∀[X:Type]. ∀[d:metric(X)].  ∀x,y:X.  ((d x y) = (d y x))
BY
{ (Auto
   THEN D 2
   THEN (Unhide THEN Auto)
   THEN ((Assert (d y x) ≤ ((d y y) + (d x y)) BY Auto) THEN (RWO "4" (-1) THENA Auto))
   THEN ((Assert (d x y) ≤ ((d x x) + (d y x)) BY Auto) THEN (RWO "4" (-1) THENA Auto))
   THEN (BLemma `rleq_antisymmetry` THENA Auto)) }

1
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 x y) ≤ (d y x)

2
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)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].    \mforall{}x,y:X.    ((d  x  y)  =  (d  y  x))


By

---

Latex:
(Auto
  THEN  D  2
  THEN  (Unhide  THEN  Auto)
  THEN  ((Assert  (d  y  x)  \mleq{}  ((d  y  y)  +  (d  x  y))  BY  Auto)  THEN  (RWO  "4"  (-1)  THENA  Auto))
  THEN  ((Assert  (d  x  y)  \mleq{}  ((d  x  x)  +  (d  y  x))  BY  Auto)  THEN  (RWO  "4"  (-1)  THENA  Auto))
  THEN  (BLemma  `rleq\_antisymmetry`  THENA  Auto))

---

Home Index