---

Step * of Lemma rccp-dist-positive

∀k:ℕ
  ∀[n:ℕ]
    ∀K:{K:n-dim-complex| 0 < ||K||} . ∀x:ℝ^k.
      (r0 < dist(x, |K|) ⇐⇒ ∃n:ℕ+. ∀p:|K|. ((r1/r(n)) ≤ mdist(rn-prod-metric(k);x;p)))
BY
{ ((UnivCD THENA Auto)
   THEN (InstLemma `compact-dist-positive` [⌜ℝ^k⌝;⌜rn-prod-metric(k)⌝;⌜|K|⌝;⌜rccp-compact(k;K)⌝;⌜x⌝]⋅ THENA Auto)
   THEN Fold `rccp-dist` (-1)
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}
    \mforall{}[n:\mBbbN{}]
        \mforall{}K:\{K:n-dim-complex|  0  <  ||K||\}  .  \mforall{}x:\mBbbR{}\^{}k.
            (r0  <  dist(x,  |K|)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}p:|K|.  ((r1/r(n))  \mleq{}  mdist(rn-prod-metric(k);x;p)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (InstLemma  `compact-dist-positive`  [\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  Trivial)

---

Home Index