compContinuousLinearMap_applyComposition

English

If p is a formal multilinear series and f: E →L F is a continuous linear map, then applying f before composing yields the same as composing with f after the composition: (p∘f) .applyComposition c v = p.applyComposition c (f ∘ v).

Русский

Если p — формальный много-линейный ряд и f: E →L F — непрерывно-линейное отображение, то применение f до композиции эквивалентно композиции после: (p∘f).applyComposition c v = p.applyComposition c (f ∘ v).

LaTeX

$$$(p.compContinuousLinearMap\\ f).applyComposition\\ c\\ v = p.applyComposition\\ c\\ (f\\circ v).$$$

Lean4

@[simp]
theorem compContinuousLinearMap_applyComposition {n : ℕ} (p : FormalMultilinearSeries 𝕜 F G) (f : E →L[𝕜] F)
    (c : Composition n) (v : Fin n → E) :
    (p.compContinuousLinearMap f).applyComposition c v = p.applyComposition c (f ∘ v) :=
  by
  ext
  simp [applyComposition, Function.comp_def]

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