LSeriesHasSum_iff — Mathlib

English

LSeriesHasSum f s a is equivalent to LSeriesSummable f s and LSeries f s = a.

Русский

LSeriesHasSum f s a эквивалентна LSeriesSummable f s и LSeries f s = a.

LaTeX

$$LSeriesHasSum(f,s,a) ⇔ (LSeriesSummable(f,s) ∧ LSeries(f,s)=a)$$

Lean4

theorem LSeriesHasSum_iff {f : ℕ → ℂ} {s a : ℂ} : LSeriesHasSum f s a ↔ LSeriesSummable f s ∧ LSeries f s = a :=
  ⟨fun H ↦ ⟨H.LSeriesSummable, H.LSeries_eq⟩, fun ⟨H₁, H₂⟩ ↦ H₂ ▸ H₁.LSeriesHasSum⟩

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