---

Step * of Lemma msep-or

∀[X:Type]. ∀d:metric(X). ∀x,y:X.  (x # y ⇒ (∀z:X. (x # z ∨ z # y)))
BY
{ (Auto
   THEN (InstLemma  `mdist-triangle-inequality` [⌜X⌝;⌜d⌝;⌜x⌝;⌜z⌝;⌜y⌝]⋅ THENA Auto)
   THEN (Assert r0 < mdist(d;x;y) BY
               (Fold `msep` 0 THEN Auto))
   THEN (Assert r0 < (mdist(d;x;z) + mdist(d;z;y)) BY
               Auto)) }

1
1. [X] : Type
2. d : metric(X)
3. x : X
4. y : X
5. x # y
6. z : X
7. mdist(d;x;y) ≤ (mdist(d;x;z) + mdist(d;z;y))
8. r0 < mdist(d;x;y)
9. r0 < (mdist(d;x;z) + mdist(d;z;y))
⊢ x # z ∨ z # y

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}d:metric(X).  \mforall{}x,y:X.    (x  \#  y  {}\mRightarrow{}  (\mforall{}z:X.  (x  \#  z  \mvee{}  z  \#  y)))


By

---

Latex:
(Auto
  THEN  (InstLemma    `mdist-triangle-inequality`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  r0  <  mdist(d;x;y)  BY
                          (Fold  `msep`  0  THEN  Auto))
  THEN  (Assert  r0  <  (mdist(d;x;z)  +  mdist(d;z;y))  BY
                          Auto))

---

Home Index