English
The dfinsuppFamily map respects composition with a left single linear map: composing f with a left single aligns with a left single composition of dfinsuppFamily f.
Русский
dfinsuppFamily сохраняет композицию с левой единичной линейной отображением: композиция f слева с единичной левой соответствует dfinsuppFamily.
LaTeX
$$$\mathrm{dfinsuppFamily}(f)\circ\mathrm{compLinearMap}(\lambda i => \DFinsupp.lsingle(p i)) = (\DFinsupp.lsingle p)\circ_{multilinear} (f p).$$$
Lean4
/-- When only one member of the family of multilinear maps is nonzero, the result consists only of
the component from that member. -/
@[simp]
theorem piFamily_single_left_apply [Fintype ι] [∀ i, DecidableEq (κ i)] (p : Π i, κ i)
(f : MultilinearMap R (fun i ↦ M i (p i)) (N p)) (x : Π i j, M i j) :
piFamily (Pi.single p f) x = Pi.single p (f fun i => x i (p i)) :=
by
ext p'
obtain rfl | hp := eq_or_ne p p'
· simp
· simp [hp]
