---

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

No Annotations
∀[X:Type]. ∀[d:metric(X)]. ∀[c:X]. ∀[r:ℝ].
  m-sphere(X;d;c;r) ⊆r m-boundary(X;d;m-ball(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 THENA Auto)
   THEN D -1
   THEN MemTypeCD
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (InstHyp [⌜c⌝;⌜x⌝;⌜M⌝] 5⋅ THENA Auto)
   THEN ExRepD
   THEN FHyp (-5) [-1]
   THEN Auto
   THEN MemTypeHD (-1)
   THEN Auto) }

1
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;c;y) ≤ r
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[c:X].  \mforall{}[r:\mBbbR{}].
    m-sphere(X;d;c;r)  \msubseteq{}r  m-boundary(X;d;m-ball(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  THENA  Auto)
  THEN  D  -1
  THEN  MemTypeCD
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (InstHyp  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}M\mkleeneclose{}]  5\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  FHyp  (-5)  [-1]
  THEN  Auto
  THEN  MemTypeHD  (-1)
  THEN  Auto)

---

Home Index