---

Step * of Lemma real-unit-ball-0

B(0) ≡ Top
BY
{ (RepeatFor 2 ((D 0 THEN Auto))
   THEN RepUR ``real-unit-ball real-vec`` 0
   THEN MemTypeCD
   THEN Auto
   THEN Try ((FunExt THEN Auto))) }

1
.....set predicate..... 
1. x : Top
⊢ ||x|| ≤ r1

---

Latex:

---

Latex:
B(0)  \mequiv{}  Top


By

---

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

---

Home Index