English
Multiplying two summable families by bilinear scalar coefficients restricts the support to a finite product of co-supports.
Русский
Умножение двух суммируемых семейств скалярным множителем ограничивает множество опор до конечного произведения ко-опор.
LaTeX
$$$ \mathrm{Supp}\bigl(i \mapsto (s(i.1).coeff(gh.1) \cdot (t(i.2).coeff(gh.2))\bigr) \subseteq (s.finite\_co\_support'(gh.1) \times t.finite\_co\_support'(gh.2))^{\mathrm{Finset}} $$$
Lean4
theorem smul_support_subset_prod (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (gh : Γ × Γ') :
(Function.support fun (i : α × β) ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆
((s.finite_co_support' gh.1).prod (t.finite_co_support' gh.2)).toFinset :=
by
intro _ hab
simp_all only [Function.mem_support, ne_eq, Set.Finite.coe_toFinset, Set.mem_prod, Set.mem_setOf_eq]
exact ⟨left_ne_zero_of_smul hab, right_ne_zero_of_smul hab⟩
