---

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


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)) ≤ (mdist(d;p;m2 n (m3 p n)) + mdist(d;p;m2 m (m3 p m)))
BY
{ ((GenConclAtAddr [1;2] THENA Auto) THEN (GenConclAtAddr [1;3] THENA Auto) THEN All Thin) }

1
1. X : Type
2. d : metric(X)
3. p : X
4. v : X
5. v1 : X
⊢ mdist(d;v;v1) ≤ (mdist(d;p;v) + mdist(d;p;v1))

---

Latex:

---

Latex:

1.  X  :  Type
2.  d  :  metric(X)
3.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
4.  m2  :  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B  k  {}\mrightarrow{}  X
5.  m3  :  X  {}\mrightarrow{}  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B  k
6.  p  :  X
7.  n  :  \mBbbN{}
8.  m  :  \mBbbN{}
9.  \mforall{}k:\mBbbN{}.  (mdist(d;p;m2  k  (m3  p  k))  \mleq{}  (r1/r(k  +  1)))
\mvdash{}  mdist(d;m2  n  (m3  p  n);m2  m  (m3  p  m))  \mleq{}  (mdist(d;p;m2  n  (m3  p  n))  +  mdist(d;p;m2  m  (m3  p  m)))


By

---

Latex:
((GenConclAtAddr  [1;2]  THENA  Auto)  THEN  (GenConclAtAddr  [1;3]  THENA  Auto)  THEN  All  Thin)

---

Home Index