summable_iff_summable_coeff — Mathlib

English

A family f is summable if and only if, for every coefficient index d, the family of coefficients coeff d (f i) is summable.

Русский

Семейство f суммируемо тогда и только тогда, когда для каждого индекса коэффициентов d семейство coeff d (f i) суммируемо.

LaTeX

$$Summable f ↔ ∀ d : σ →₀ ℕ, Summable (λ i, coeff d (f i))$$

Lean4

theorem summable_iff_summable_coeff : Summable f ↔ ∀ d : σ →₀ ℕ, Summable (fun i ↦ coeff d (f i)) :=
  by
  simp_rw [Summable, hasSum_iff_hasSum_coeff]
  constructor
  · rintro ⟨a, h⟩ n
    exact ⟨coeff n a, h n⟩
  · intro h
    choose a h using h
    exact ⟨a, by simpa using h⟩

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