isCauSeq_re — Mathlib

English

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

Русский

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

LaTeX

$$$\\mathrm{cauSeqRe}(f) = \\langle \\,\\lambda n.\\operatorname{Re}(f(n)),\\, isCauSeq\\; re\\; f \\rangle$$$

Lean4

theorem isCauSeq_re (f : CauSeq ℂ (‖·‖)) : IsCauSeq abs fun n ↦ (f n).re := fun _ ε0 ↦
  (f.cauchy ε0).imp fun i H j ij ↦ lt_of_le_of_lt (by simpa using abs_re_le_norm (f j - f i)) (H _ ij)

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