---

Step * of Lemma m-regularize_wf_finite

∀[X:Type]. ∀[d:metric(X)]. ∀[b:ℕ]. ∀[s:ℕb ⟶ X].  (m-regularize(d;s) ∈ ℕb ⟶ X)
BY
{ ProveWfLemma }

1
1. X : Type
2. d : metric(X)
3. b : ℕ
4. s : ℕb ⟶ X
5. n : ℕb
6. 0 < first-m-not-reg(d;s;n + 1)
⊢ first-m-not-reg(d;s;n + 1) - 2 ∈ ℕb

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[b:\mBbbN{}].  \mforall{}[s:\mBbbN{}b  {}\mrightarrow{}  X].    (m-regularize(d;s)  \mmember{}  \mBbbN{}b  {}\mrightarrow{}  X)


By

---

Latex:
ProveWfLemma

---

Home Index