---

Step * 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))
⊢ mdist(d;c;y) ≤ r
BY
{ ((Assert mdist(d;c;y) ≤ (mdist(d;c;x) + mdist(d;x;y)) BY Auto) THEN (RWO "-1" 0 THENA Auto)) }

1
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

---

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))
\mvdash{}  mdist(d;c;y)  \mleq{}  r


By

---

Latex:
((Assert  mdist(d;c;y)  \mleq{}  (mdist(d;c;x)  +  mdist(d;x;y))  BY  Auto)  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index