smul_support_finite — Mathlib

English

The support of the pointwise product of two summable families is finite.

Русский

Поддержка точечного произведения двух суммируемых семейств конечна.

LaTeX

$$$ (\mathrm{Supp}\ \bigl(i \mapsto (s(i.1).coeff(gh.1) \cdot (t(i.2).coeff(gh.2))\bigr)).Finite $$$

Lean4

theorem smul_support_finite (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (gh : Γ × Γ') :
    (Function.support fun (i : α × β) ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2).Finite :=
  Set.Finite.subset (Set.toFinite ((s.finite_co_support' gh.1).prod (t.finite_co_support' gh.2)).toFinset)
    (smul_support_subset_prod s t gh)

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