---

Step * of Lemma m-ball-boundary

No Annotations
∀[X:Type]. ∀[d:metric(X)]. ∀[c:X]. ∀[r:ℝ].
  m-boundary(X;d;m-ball(X;d;c;r)) ≡ m-sphere(X;d;c;r) 
  supposing ∀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))))
BY
{ (Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[c:X].  \mforall{}[r:\mBbbR{}].
    m-boundary(X;d;m-ball(X;d;c;r))  \mequiv{}  m-sphere(X;d;c;r) 
    supposing  \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))))


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index