English
Sums over the vAddAntidiagonal with bilinear coefficients decompose across the independent indices.
Русский
Суммирование по диагонали vAddAntidiagonal разбивается по независимым индексам.
LaTeX
$$$ \sum_{x \in VAddAntidiagonal (s a.1).isPWO\_support' (t a.2).isPWO\_support' g} (s a.1).coeff x.1 \cdot (t a.2).coeff x.2 = \sum_{x \in VAddAntidiagonal s.isPWO_iUnion_support' t.isPWO_iUnion_support' g} (s a.1).coeff x.1 \cdot (t a.2).coeff x.2$$$
Lean4
theorem finite_co_support_prod_smul (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) (g : Γ') :
Finite {(ab : α × β) | ((fun (ab : α × β) ↦ (of R).symm (s ab.1 • (of R) (t ab.2))) ab).coeff g ≠ 0} :=
by
apply
((VAddAntidiagonal s.isPWO_iUnion_support t.isPWO_iUnion_support g).finite_toSet.biUnion'
(fun gh _ => smul_support_finite s t gh)).subset
_
exact fun ab hab => by
simp only [ne_eq, Set.mem_setOf_eq] at hab
obtain ⟨ij, hij⟩ := Finset.exists_ne_zero_of_sum_ne_zero hab
simp only [mem_coe, mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq, Function.mem_support, exists_prop,
Prod.exists]
exact
⟨ij.1, ij.2,
⟨⟨ab.1, left_ne_zero_of_smul hij.2⟩, ⟨ab.2, right_ne_zero_of_smul hij.2⟩,
((mem_vaddAntidiagonal _ _ _).mp hij.1).2.2⟩,
hij.2⟩
