---

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


1. X : Type
2. d : metric(X)
3. c : X
4. r : ℝ
5. x : X
6. mdist(d;c;x) ≤ r
7. mdist(d;c;x) < r
8. k : ℕ+
9. (r1/r(k)) < (r - mdist(d;c;x))
10. y : X
11. mdist(d;y;x) ≤ (r1/r(k))
12. mdist(d;c;y) ≤ (mdist(d;c;x) + mdist(d;x;y))
⊢ (mdist(d;c;x) + mdist(d;x;y)) ≤ r
BY
{ ((RWO "mdist-symm" (-2) THENA Auto) THEN RWW  "-2 -4" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  c  :  X
4.  r  :  \mBbbR{}
5.  x  :  X
6.  mdist(d;c;x)  \mleq{}  r
7.  mdist(d;c;x)  <  r
8.  k  :  \mBbbN{}\msupplus{}
9.  (r1/r(k))  <  (r  -  mdist(d;c;x))
10.  y  :  X
11.  mdist(d;y;x)  \mleq{}  (r1/r(k))
12.  mdist(d;c;y)  \mleq{}  (mdist(d;c;x)  +  mdist(d;x;y))
\mvdash{}  (mdist(d;c;x)  +  mdist(d;x;y))  \mleq{}  r


By

---

Latex:
((RWO  "mdist-symm"  (-2)  THENA  Auto)  THEN  RWW    "-2  -4"  0  THEN  Auto)

---

Home Index