isCauSeq_im — Mathlib

English

The imaginary part of a complex Cauchy sequence is a real Cauchy sequence: cauSeqIm(f) is a CauSeq in ℝ with abs.

Русский

Мнимая часть комплексной последовательности Коши является последовательностью действительных чисел: cauSeqIm(f) является CauSeq в ℝ с модулем abs.

LaTeX

$$$\\mathrm{cauSeqIm}(f) = \\langle \\,\\lambda n.\\operatorname{Im}(f(n)),\\, isCauSeq\\; im\\; f \\rangle$$$

Lean4

theorem isCauSeq_im (f : CauSeq ℂ (‖·‖)) : IsCauSeq abs fun n ↦ (f n).im := fun ε ε0 ↦
  (f.cauchy ε0).imp fun i H j ij ↦ by
    simpa only [← ofReal_sub, norm_real, sub_re] using (abs_im_le_norm _).trans_lt <| H _ ij

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