English
The dfinsuppFamily of a Pi.single map equals the left-hand-side composition: (DSingle) ∘ MultilinearMap (f p) with appropriate lapply projections.
Русский
DFinsuppFamily для Pi.single отображения эквивалентно композиции слева: DFinsupp-левый элемент ∘ мультиленейное отображение (f p) с проекциями lapply.
LaTeX
$$$\dfinsuppFamily (\Pi.single p f) = (\DFinsupp.lsingle p).compMultilinearMap (f.compLinearMap (\lambda i => \DFinsupp.lapply (p i))).$$$
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 dfinsuppFamily_single_left_apply [∀ i, DecidableEq (κ i)] (p : Π i, κ i)
(f : MultilinearMap R (fun i ↦ M i (p i)) (N p)) (x : Π i, Π₀ j, M i j) :
dfinsuppFamily (Pi.single p f) x = DFinsupp.single p (f fun i => x _ (p i)) :=
by
ext p'
obtain rfl | hp := eq_or_ne p p'
· simp
· simp [hp]
