---

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

No Annotations
∀[X:Type]. ∀[d:metric(X)]. ∀[c:X]. ∀[r:ℝ].  (m-boundary(X;d;m-ball(X;d;c;r)) ⊆r m-sphere(X;d;c;r))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN DVar `x'
   THEN (BLemma `not-rneq` THENA Auto)
   THEN ParallelLast
   THEN D -1
   THEN ((Assert ⌜False⌝⋅ THEN Complete (Auto))
   ORELSE ((InstLemma `small-reciprocal-real` [⌜r - mdist(d;c;x)⌝]⋅ THENA Auto)
           THEN UnfoldTopAb 0
           THEN ParallelLast
           THEN Auto
           THEN MemTypeCD
           THEN Auto
           THEN RenameVar `y' (-2))
   )) }

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))
⊢ mdist(d;c;y) ≤ r

---

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))  \msubseteq{}r  m-sphere(X;d;c;r))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  DVar  `x'
  THEN  (BLemma  `not-rneq`  THENA  Auto)
  THEN  ParallelLast
  THEN  D  -1
  THEN  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto))
  ORELSE  ((InstLemma  `small-reciprocal-real`  [\mkleeneopen{}r  -  mdist(d;c;x)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                  THEN  UnfoldTopAb  0
                  THEN  ParallelLast
                  THEN  Auto
                  THEN  MemTypeCD
                  THEN  Auto
                  THEN  RenameVar  `y'  (-2))
  ))

---

Home Index