English
If you apply dfinsuppFamily to a left-side singleton family, you obtain a single dfinsupp factor carrying the result of f p on the corresponding m.
Русский
При применении dfinsuppFamily к левосторонней единичной семье получается один DFinsupp-элемент, неся результат отображения f p на соответствующем m.
LaTeX
$$$\dfinsuppFamily (\Pi.single p f)\ (\lambda i \mapsto m(i)) = \DFinsupp.single\ p\ (f\ p\ m).$$$
Lean4
/-- When applied to a family of finitely-supported functions each supported on a single element,
`dfinsuppFamily` is itself supported on a single element, with value equal to the map `f` applied
at that point. -/
@[simp]
theorem dfinsuppFamily_single [∀ i, DecidableEq (κ i)]
(f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) (p : ∀ i, κ i) (m : ∀ i, M i (p i)) :
dfinsuppFamily f (fun i => .single (p i) (m i)) = DFinsupp.single p (f p m) :=
by
ext q
obtain rfl | hpq := eq_or_ne q p
· simp
· rw [DFinsupp.single_eq_of_ne hpq]
rw [Function.ne_iff] at hpq
obtain ⟨i, hpqi⟩ := hpq
apply (f q).map_coord_zero i
simp_rw [DFinsupp.single_eq_of_ne hpqi]
