isCauSeq_im — Mathlib

English

The imaginary part sequence of a CauSeq is a CauSeq with abs metric: IsCauSeq abs (im ∘ f).

Русский

Последовательность мнимой части CauSeq имеет метрику abs: IsCauSeq abs (im ∘ f).

LaTeX

$$$$ \\text{IsCauSeq abs } (\\operatorname{im} \\circ f). $$$$

Lean4

theorem isCauSeq_im (f : CauSeq K norm) : IsCauSeq abs fun n => im (f n) := fun _ ε0 =>
  (f.cauchy ε0).imp fun i H j ij => lt_of_le_of_lt (by simpa only [map_sub] using abs_im_le_norm (f j - f i)) (H _ ij)

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