---

Step * of Lemma m-regular-not-m-not-reg

∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X].  (m-k-regular(d;2;s) ⇒ (∀n:ℕ. m-not-reg(d;s;n) = ff))
BY
{ Auto }

1
1. X : Type
2. d : metric(X)
3. s : ℕ ⟶ X
4. m-k-regular(d;2;s)
5. n : ℕ
⊢ m-not-reg(d;s;n) = ff

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].    (m-k-regular(d;2;s)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  m-not-reg(d;s;n)  =  ff))


By

---

Latex:
Auto

---

Home Index