compContinuousLinearMap_apply — Mathlib

English

If p = p1 and u = u1, then p.compContinuousLinearMap u = p1.compContinuousLinearMap u1; in particular, when using identical data the results are identical.

Русский

Если p = p1 и u = u1, то p.compContinuousLinearMap u = p1.compContinuousLinearMap u1; то есть при идентичности данных результат совпадает.

LaTeX

$$p = p1 → u = u1 → p.compContinuousLinearMap u = p1.compContinuousLinearMap u1$$

Lean4

@[simp]
theorem compContinuousLinearMap_apply (p : FormalMultilinearSeries 𝕜 F G) (u : E →L[𝕜] F) (n : ℕ) (v : Fin n → E) :
    (p.compContinuousLinearMap u) n v = p n (u ∘ v) :=
  rfl

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