---

Step * 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)) ≤ ((r1/r(n + 1)) + (r1/r(m + 1)))
BY
{ (RWO "-1<" 0 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)) ≤ (mdist(d;p;m2 n (m3 p n)) + mdist(d;p;m2 m (m3 p m)))

---

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{}  ((r1/r(n  +  1))  +  (r1/r(m  +  1)))


By

---

Latex:
(RWO  "-1<"  0  THENA  Auto)

---

Home Index