compFormalMultilinearSeries_apply'

English

Left-composing a formal multilinear series with a continuous linear map f yields a new formal multilinear series whose nth term is f ∘ p(n).

Русский

Преобразование, получающее новый формальный мультилинейный ряд путём композиции каждого члена p(n) с непрерывной линейной картой f: (f ∘ p)(n) = f ∘ p(n).

LaTeX

$$$(f \\circ_{\\mathrm{FM}} p)(n) = f \\circ p(n)$$$

Lean4

theorem compFormalMultilinearSeries_apply' (f : F →L[𝕜] G) (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (v : Fin n → E) :
    (f.compFormalMultilinearSeries p) n v = f (p n v) :=
  rfl

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