---

Step * of Lemma rccp-dist-0

∀[k,n:ℕ]. ∀[K:{K:n-dim-complex| 0 < ||K||} ]. ∀[x:ℝ^k].  uiff(dist(x, |K|) = r0;x ∈ |K|)
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `compact-dist-zero-in-complete` [⌜ℝ^k⌝;⌜rn-prod-metric(k)⌝;⌜|K|⌝;⌜rccp-compact(k;K)⌝;⌜x⌝]⋅
         THENA Auto
         )
   THEN Fold `rccp-dist` (-1)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k,n:\mBbbN{}].  \mforall{}[K:\{K:n-dim-complex|  0  <  ||K||\}  ].  \mforall{}[x:\mBbbR{}\^{}k].    uiff(dist(x,  |K|)  =  r0;x  \mmember{}  |K|)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `compact-dist-zero-in-complete`  [\mkleeneopen{}\mBbbR{}\^{}k\mkleeneclose{};\mkleeneopen{}rn-prod-metric(k)\mkleeneclose{};\mkleeneopen{}|K|\mkleeneclose{};
              \mkleeneopen{}rccp-compact(k;K)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Fold  `rccp-dist`  (-1)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index