---

Step * of Lemma real-ball-0

∀[r:{r:ℝ| r0 ≤ r} ]. B(0;r) ≡ Top
BY
{ (RepeatFor 3 ((D 0 THEN Auto))
   THEN RepUR ``real-ball real-vec`` 0
   THEN MemTypeCD
   THEN Auto
   THEN Try ((FunExt THEN Auto))) }

1
.....set predicate..... 
1. r : {r:ℝ| r0 ≤ r} 
2. x : Top
⊢ ||x|| ≤ r

---

Latex:

---

Latex:
\mforall{}[r:\{r:\mBbbR{}|  r0  \mleq{}  r\}  ].  B(0;r)  \mequiv{}  Top


By

---

Latex:
(RepeatFor  3  ((D  0  THEN  Auto))
  THEN  RepUR  ``real-ball  real-vec``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Try  ((FunExt  THEN  Auto)))

---

Home Index