---

Step * of Lemma mtb-point-cantor-seq-regular

∀[X:Type]. ∀[d:metric(X)].  ∀mtb:m-TB(X;d). ∀p:X.  m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;p)))
BY
{ (Intros
   THEN RepeatFor 2 (DVar `mtb')
   THEN (D -3 THEN Reduce -2)
   THEN RepUR ``mtb-seq mtb-point-cantor`` 0
   THEN D 0
   THEN Auto
   THEN Reduce 0
   THEN (D 6 With ⌜p⌝  THENA Auto)) }

1
1. X : Type
2. d : metric(X)
3. B : ℕ ⟶ ℕ+
4. m2 : k:ℕ ⟶ ℕB k ⟶ X
5. m3 : X ⟶ k:ℕ ⟶ ℕB k
6. p : X
7. n : ℕ
8. m : ℕ
9. ∀k:ℕ. (mdist(d;p;m2 k (m3 p k)) ≤ (r1/r(k + 1)))
⊢ mdist(d;m2 n (m3 p n);m2 m (m3 p m)) ≤ ((r1/r(n + 1)) + (r1/r(m + 1)))

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].
    \mforall{}mtb:m-TB(X;d).  \mforall{}p:X.    m-k-regular(d;1;mtb-seq(mtb;mtb-point-cantor(mtb;p)))


By

---

Latex:
(Intros
  THEN  RepeatFor  2  (DVar  `mtb')
  THEN  (D  -3  THEN  Reduce  -2)
  THEN  RepUR  ``mtb-seq  mtb-point-cantor``  0
  THEN  D  0
  THEN  Auto
  THEN  Reduce  0
  THEN  (D  6  With  \mkleeneopen{}p\mkleeneclose{}    THENA  Auto))

---

Home Index