English
Assuming decidable equality and nonzero-sensing conditions on the coordinates, the support of dfinsuppFamily f applied to x is contained in the product of the supports of each x(i).
Русский
При предположении о разрешимости равенств и условиях ненулевых координат, поддержка dfinsuppFamily f применённого к x содержится в произведении опор всех x(i).
LaTeX
$$$\mathrm{supp}(\dfinsuppFamily f\, x) \subseteq \prod_{i} \mathrm{supp}(x(i)).$$$
Lean4
theorem support_dfinsuppFamily_subset [∀ i, DecidableEq (κ i)] [∀ i j, (x : M i j) → Decidable (x ≠ 0)]
[∀ i, (x : N i) → Decidable (x ≠ 0)] (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p))
(x : ∀ i, Π₀ j : κ i, M i j) : (dfinsuppFamily f x).support ⊆ Fintype.piFinset fun i => (x i).support :=
by
intro p hp
simp only [DFinsupp.mem_support_toFun, dfinsuppFamily_apply_toFun, ne_eq, Fintype.mem_piFinset] at hp ⊢
intro i
exact mt ((f p).map_coord_zero (m := fun i => x i _) i) hp
