---

Step * of Lemma meq-equiv

∀[X:Type]. ∀[d:metric(X)].  EquivRel(X;x,y.x ≡ y)
BY
{ (InstLemma `metric-symmetry` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Unfold `meq` 0
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN Try ((Unhide THEN Auto))
   THEN DVar `d'
   THEN Unhide
   THEN Auto
   THEN Try ((RWO "5" 0 THEN Complete (Auto)))
   THEN BLemma `rleq_antisymmetry`
   THEN 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,y:X.  ((d x y) = (d y x))
6. Sym(X;x,y.(d x y) = r0)
7. a : X
8. b : X
9. c : X
10. (d a b) = r0
11. (d b c) = r0
⊢ (d a c) ≤ r0

---

Latex:

---

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


By

---

Latex:
(InstLemma  `metric-symmetry`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Unfold  `meq`  0
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  Try  ((Unhide  THEN  Auto))
  THEN  DVar  `d'
  THEN  Unhide
  THEN  Auto
  THEN  Try  ((RWO  "5"  0  THEN  Complete  (Auto)))
  THEN  BLemma  `rleq\_antisymmetry`
  THEN  Auto)

---

Home Index