lift_comp_map — Mathlib

English

If h is a multilinear map from t to E, then lifting h after applying map f equals lifting the composition h ∘ f at the level of multilinear maps: lift h ∘ map f = lift (h ∘ LinearMap f).

Русский

Если h — мультилинейное отображение t → E, то подъем (lifting) после применения map f равен подъему композиции h с f: lift h ∘ map f = lift (h ∘ LinearMap f).

LaTeX

$$$\mathrm{lift}\, h \circ_\ell \mathrm{map}\, f = \mathrm{lift}\, (h \circ_{\\text{LinearMap}} f)$$$

Lean4

theorem lift_comp_map (h : MultilinearMap R t E) : lift h ∘ₗ map f = lift (h.compLinearMap f) :=
  by
  ext
  simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, Function.comp_apply, map_tprod, lift.tprod,
    MultilinearMap.compLinearMap_apply]

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