English
The dfinsuppFamily applied to a left single element yields a single DFinsupp with the image of f applied to the left coordinate.
Русский
DFinsuppFamily, применяемая к левому одиночному элементу, дает одиночный DFinsupp с образом f на левой координате.
LaTeX
$$$\dfinsuppFamily (\Pi.single p f)\ (\lambda i => .single (p i) (m i)) = DFinsupp.single p (f p m).$$$
Lean4
/-- When applied to a family of finitely-supported functions each supported on a single element,
`piFamily` is itself supported on a single element, with value equal to the map `f` applied
at that point. -/
@[simp]
theorem piFamily_single [Fintype ι] [∀ 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)) :
piFamily f (fun i => Pi.single (p i) (m i)) = Pi.single p (f p m) :=
by
ext q
obtain rfl | hpq := eq_or_ne p q
· simp
· rw [Pi.single_eq_of_ne' hpq]
rw [Function.ne_iff] at hpq
obtain ⟨i, hpqi⟩ := hpq
apply (f q).map_coord_zero i
simp_rw [Pi.single_eq_of_ne' hpqi]
