finite_co_support_prod_mul — Mathlib

English

The finite co-support for the product of two summable families is guaranteed for each fixed g.

Русский

Для каждого фиксированного g существует конечная ко-поддержка произведения двух суммируемых семейств.

LaTeX

$$$ finite\_co\_support\_prod\_mul (s) (t) (g) : Finite \{(a,b) \mid ((s a.1 * t a.2)).coeff g \neq 0\} $$$

Lean4

theorem finite_co_support_prod_mul (s : SummableFamily Γ R α) (t : SummableFamily Γ R β) (g : Γ) :
    Finite {(a : α × β) | ((fun (a : α × β) ↦ (s a.1 * t a.2)) a).coeff g ≠ 0} :=
  finite_co_support_prod_smul s t g

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