comp_comp — Mathlib

English

The seminorm of a sum of two maps composes additively: (p + q) ∘ f = p ∘ f + q ∘ f.

Русский

Полунормa суммы отображений композируется аддитивно: (p + q) ∘ f = p ∘ f + q ∘ f.

LaTeX

$$$ (p + q) \circ f = p \circ f + q \circ f $$$

Lean4

theorem comp_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (p : Seminorm 𝕜₃ E₃) (g : E₂ →ₛₗ[σ₂₃] E₃) (f : E →ₛₗ[σ₁₂] E₂) :
    p.comp (g.comp f) = (p.comp g).comp f :=
  ext fun _ => rfl

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