piFamily_single_left — Mathlib

English

A single left coordinate map is carried through piFamily to a single coordinate in the product, matching the f p evaluation.

Русский

Левая единичная координатная карта переносится через piFamily в единичную координату произведения, совпадая с f p вычислением.

LaTeX

$$$\mathrm{piFamily}(\Pi.single p f) = (\mathrm{LinearMap.single}\ R\ N\ p) \circ_{multilinear} (f\ p \circ \mathrm{proj}(p i)).$$$

Lean4

theorem piFamily_single_left [Fintype ι] [∀ i, DecidableEq (κ i)] (p : Π i, κ i)
    (f : MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
    piFamily (Pi.single p f) = (LinearMap.single R _ p).compMultilinearMap (f.compLinearMap fun i => .proj (p i)) :=
  ext <| piFamily_single_left_apply _ _

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