---

Step * of Lemma m-regularize-of-regular

∀[X:Type]. ∀[d:metric(X)]. ∀[s:ℕ ⟶ X].  m-regularize(d;s) = s ∈ (ℕ ⟶ X) supposing m-k-regular(d;2;s)
BY
{ (Auto THEN (InstLemma `m-regular-not-m-not-reg` [⌜X⌝;⌜d⌝;⌜s⌝]⋅ THENA Auto) THEN (FunExt THENA 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
6. x : ℕ
⊢ (m-regularize(d;s) x) = (s x) ∈ X

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[s:\mBbbN{}  {}\mrightarrow{}  X].    m-regularize(d;s)  =  s  supposing  m-k-regular(d;2;s)


By

---

Latex:
(Auto  THEN  (InstLemma  `m-regular-not-m-not-reg`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (FunExt  THENA  Auto))

---

Home Index