compContinuousLinearMap — Mathlib

English

The coercion map composes with pi: the evaluation map on the pi-construction equals evaluation on the corresponding component.

Русский

Связующее отображение согласуется с pi: оценка через pi равна оценке через компоненту.

LaTeX

$$$\\text{coe}_\\pi = \\text{pi}_{*}$.$$

Lean4

/-- If `g` is continuous multilinear and `f` is a collection of continuous linear maps,
then `g (f₁ m₁, ..., fₙ mₙ)` is again a continuous multilinear map, that we call
`g.compContinuousLinearMap f`. -/
def compContinuousLinearMap (g : ContinuousMultilinearMap R M₁' M₄) (f : ∀ i : ι, M₁ i →L[R] M₁' i) :
    ContinuousMultilinearMap R M₁ M₄ :=
  { g.toMultilinearMap.compLinearMap fun i => (f i).toLinearMap with
    cont := g.cont.comp <| continuous_pi fun j => (f j).cont.comp <| continuous_apply _ }

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