compContinuousAlternatingMap — Mathlib

English

The evaluation of the composed map at a vector equals applying the inner map to the vector components.

Русский

Оценка составленного отображения на вектор равна применению внутреннего отображения к компонентам вектора.

LaTeX

$$$ g (f m) = g(\\,m) \\circ f $$$

Lean4

/-- Composing a continuous alternating map with a continuous linear map gives again a
continuous alternating map. -/
def _root_.ContinuousLinearMap.compContinuousAlternatingMap (g : N →L[R] N') (f : M [⋀^ι]→L[R] N) : M [⋀^ι]→L[R] N' :=
  { (g : N →ₗ[R] N').compAlternatingMap f.toAlternatingMap with
    toContinuousMultilinearMap := g.compContinuousMultilinearMap f.1 }

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