isCauSeq_exp — Mathlib

English

For any z ∈ ℂ, the partial sums s_n = ∑_{m=0}^{n-1} z^m / m! form a Cauchy sequence in ℂ with respect to the complex norm.

Русский

Для любого z ∈ ℂ частичные суммы s_n = \\sum_{m=0}^{n-1} z^m / m! образуют последовательность Коши в \\ℂ по норме.

LaTeX

$$$\\forall z\\in\\mathbb{C},\\; IsCauSeq\\; \\|\\cdot\\|\\ (n \\mapsto \\sum_{m=0}^{n-1} z^m / m!)$$$

Lean4

theorem isCauSeq_exp (z : ℂ) : IsCauSeq (‖·‖) fun n => ∑ m ∈ range n, z ^ m / m.factorial :=
  (isCauSeq_norm_exp z).of_abv

Похожие утверждения