LSeriesSummable_iff_of_re_eq_re — Mathlib

English

If Re(s) = Re(s'), then LSeriesSummable f s ⇔ LSeriesSummable f s'.

Русский

Если Re(s) = Re(s'), то LSeriesSummable f s эквивалентна LSeriesSummable f s'.

LaTeX

$$(s.re = s'.re) → (LSeriesSummable(f,s) ↔ LSeriesSummable(f,s'))$$

Lean4

theorem LSeriesSummable_iff_of_re_eq_re {f : ℕ → ℂ} {s s' : ℂ} (h : s.re = s'.re) :
    LSeriesSummable f s ↔ LSeriesSummable f s' :=
  ⟨fun H ↦ H.of_re_le_re h.le, fun H ↦ H.of_re_le_re h.symm.le⟩

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