---

Step * of Lemma fun-converges-to-cosine

No Annotations
lim n→∞.Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤n} = λx.cosine(x) for x ∈ (-∞, ∞)
BY
{ InstLemma `cosine-is-limit` []⋅ }

1
1. ∀x:ℝ. Σi.-1^i * (x^2 * i)/(2 * i)! = cosine(x)
⊢ lim n→∞.Σ{-1^i * (x^2 * i)/(2 * i)! | 0≤i≤n} = λx.cosine(x) for x ∈ (-∞, ∞)

---

Latex:

---

Latex:
No  Annotations
lim  n\mrightarrow{}\minfty{}.\mSigma{}\{-1\^{}i  *  (x\^{}2  *  i)/(2  *  i)!  |  0\mleq{}i\mleq{}n\}  =  \mlambda{}x.cosine(x)  for  x  \mmember{}  (-\minfty{},  \minfty{})


By

---

Latex:
InstLemma  `cosine-is-limit`  []\mcdot{}

---

Home Index