finite_co_support — Mathlib

English

For any summable family s and any g in Γ, the set {a | (s a).coeff g ≠ 0} is finite.

Русский

Для любой суммируемой семейства s и любого элемента g множества {a | коэффициент (s a) по g не равен нулю} конечно.

LaTeX

$$$\\{a \\mid (s(a)).{\\mathrm{coeff}}\\,g \\neq 0\\}$ is finite for each g$$

Lean4

theorem finite_co_support (s : SummableFamily Γ R α) (g : Γ) : (Function.support fun a => (s a).coeff g).Finite :=
  s.finite_co_support' g

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