summable_conj — Mathlib

English

A sequence (or function) f: α → ℂ is summable if and only if its pointwise complex conjugate is summable: Summable f ⇔ Summable conj(f).

Русский

Сходимость ряда сохраняется под взятием комплексного сопряжения: Summable f ⇔ Summable conj(f).

LaTeX

$$$ (\\text{Summable } f) \\iff (\\text{Summable } \\overline{f}) $$$

Lean4

theorem summable_conj {f : α → ℂ} : (Summable fun x => conj (f x)) ↔ Summable f :=
  RCLike.summable_conj _

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