---

Step * of Lemma not-msep

∀[X:Type]. ∀[d:metric(X)]. ∀[x,y:X].  x ≡ y supposing ¬x # y
BY
{ (Auto THEN Unfold `msep` -1 THEN (FLemma `not-rless` [-1] THENA Auto) THEN (Assert r0 ≤ mdist(d;x;y) BY Auto)) }

1
1. X : Type
2. d : metric(X)
3. x : X
4. y : X
5. ¬(r0 < mdist(d;x;y))
6. mdist(d;x;y) ≤ r0
7. r0 ≤ mdist(d;x;y)
⊢ x ≡ y

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[x,y:X].    x  \mequiv{}  y  supposing  \mneg{}x  \#  y


By

---

Latex:
(Auto
  THEN  Unfold  `msep`  -1
  THEN  (FLemma  `not-rless`  [-1]  THENA  Auto)
  THEN  (Assert  r0  \mleq{}  mdist(d;x;y)  BY
                          Auto))

---

Home Index