---

Step * of Lemma m-reg-test_wf

∀[X:Type]
  ∀d:metric(X). ∀b:ℕ. ∀s:ℕb ⟶ X. ∀x:X.
    (m-reg-test(d;b;s;x) ∈ (∃n:ℕb. (((r(2)/r(n + 1)) + (r(2)/r(b + 1))) < mdist(d;s n;x)))
     ∨ (∀n:ℕb. (mdist(d;s n;x) < ((r(3)/r(n + 1)) + (r(3)/r(b + 1))))))
BY
{ ProveWfLemma }

1
1. X : Type
2. d : metric(X)
3. b : ℕ
4. s : ℕb ⟶ X
5. x : X
6. n : ℕb
⊢ (r(3)/r(n + 1)) + (r(3)/r(b + 1)) ∈ {y:ℝ| ((r(2)/r(n + 1)) + (r(2)/r(b + 1))) < y} 

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}d:metric(X).  \mforall{}b:\mBbbN{}.  \mforall{}s:\mBbbN{}b  {}\mrightarrow{}  X.  \mforall{}x:X.
        (m-reg-test(d;b;s;x)  \mmember{}  (\mexists{}n:\mBbbN{}b.  (((r(2)/r(n  +  1))  +  (r(2)/r(b  +  1)))  <  mdist(d;s  n;x)))
          \mvee{}  (\mforall{}n:\mBbbN{}b.  (mdist(d;s  n;x)  <  ((r(3)/r(n  +  1))  +  (r(3)/r(b  +  1))))))


By

---

Latex:
ProveWfLemma

---

Home Index