---

Step * 1 1 of Lemma m-sphere-subtype-m-ball-boundary


1. X : Type
2. d : metric(X)
3. c : X
4. r : ℝ
5. ∀c,x:X. ∀M:ℕ+.
     ∃y:X. ((mdist(d;c;y) = (mdist(d;c;x) + mdist(d;x;y))) ∧ (r0 < mdist(d;y;x)) ∧ (mdist(d;y;x) ≤ (r1/r(M))))
6. x : X
7. mdist(d;c;x) = r
8. M : ℕ+
9. ∀x@0:X. ((mdist(d;x@0;x) ≤ (r1/r(M))) ⇒ (x@0 ∈ m-ball(X;d;c;r)))
10. y : X
11. mdist(d;c;y) = (mdist(d;c;x) + mdist(d;x;y))
12. r0 < mdist(d;y;x)
13. mdist(d;y;x) ≤ (r1/r(M))
14. y = y ∈ X
15. mdist(d;x;y) ≤ r0
⊢ False
BY
{ (RWO "mdist-symm" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  c  :  X
4.  r  :  \mBbbR{}
5.  \mforall{}c,x:X.  \mforall{}M:\mBbbN{}\msupplus{}.
          \mexists{}y:X
            ((mdist(d;c;y)  =  (mdist(d;c;x)  +  mdist(d;x;y)))
            \mwedge{}  (r0  <  mdist(d;y;x))
            \mwedge{}  (mdist(d;y;x)  \mleq{}  (r1/r(M))))
6.  x  :  X
7.  mdist(d;c;x)  =  r
8.  M  :  \mBbbN{}\msupplus{}
9.  \mforall{}x@0:X.  ((mdist(d;x@0;x)  \mleq{}  (r1/r(M)))  {}\mRightarrow{}  (x@0  \mmember{}  m-ball(X;d;c;r)))
10.  y  :  X
11.  mdist(d;c;y)  =  (mdist(d;c;x)  +  mdist(d;x;y))
12.  r0  <  mdist(d;y;x)
13.  mdist(d;y;x)  \mleq{}  (r1/r(M))
14.  y  =  y
15.  mdist(d;x;y)  \mleq{}  r0
\mvdash{}  False


By

---

Latex:
(RWO  "mdist-symm"  (-1)  THEN  Auto)

---

Home Index