compContinuousLinearMap_comp — Mathlib

English

For any n and v, (p.compContinuousLinearMap u) n v = p n (u ∘ v).

Русский

Для любого n и вектора v, выполняется (p.compContinuousLinearMap u) n v = p n (u ∘ v).

LaTeX

$$(p.compContinuousLinearMap u)\, n\, v = p\, n\, (u \circ v)$$

Lean4

theorem compContinuousLinearMap_comp (p : FormalMultilinearSeries 𝕜 G H) (u₁ : F →L[𝕜] G) (u₂ : E →L[𝕜] F) :
    (p.compContinuousLinearMap u₁).compContinuousLinearMap u₂ = p.compContinuousLinearMap (u₁.comp u₂) :=
  rfl

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