dfinsuppFamily_single_left — Mathlib

English

The dfinsuppFamily of a composition with a left-constructed linear map equals the composition with the left linear map and f p, i.e. the two ways of wiring the inputs agree.

Русский

DFinsuppFamily композиции с лево-сконструированной линейной картой равна композиции с левой линейной картой и f p, то есть оба способа подачи входов совпадают.

LaTeX

$$$(\dfinsuppFamily f).compLinearMap (\lambda i => \DFinsupp.lsingle (p i)) = (\DFinsupp.lsingle p).compMultilinearMap (f p).$$$

Lean4

theorem dfinsuppFamily_single_left [∀ i, DecidableEq (κ i)] (p : Π i, κ i)
    (f : MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
    dfinsuppFamily (Pi.single p f) =
      (DFinsupp.lsingle p).compMultilinearMap (f.compLinearMap fun i => DFinsupp.lapply (p i)) :=
  ext <| dfinsuppFamily_single_left_apply _ _

Похожие утверждения