English
exp'(z) is defined as the Cauchy sequence of partial sums of the Taylor series of e^z; the nth term is ∑_{m< n} z^m / m! and is known to be a Cauchy sequence.
Русский
exp'(z) задаётся как Cauchy-последовательность частичных сумм разложения e^z в Тейлоровом ряде; n-й член равен сумме по m < n.
LaTeX
$$$\\text{exp}'(z) := \\langle n \\mapsto \\sum_{m=0}^{n-1} \\frac{z^m}{m!},\\; IsCauSeq\\; (abs)\\ (n \\mapsto \\sum_{m=0}^{n-1} \\frac{|z|^m}{m!}) \\rangle$$$
Lean4
/-- The Cauchy sequence consisting of partial sums of the Taylor series of
the complex exponential function -/
@[pp_nodot]
def exp' (z : ℂ) : CauSeq ℂ (‖·‖) :=
⟨fun n => ∑ m ∈ range n, z ^ m / m.factorial, isCauSeq_exp z⟩
