comp_smul_apply — Mathlib

English

For a seminorm p on E2 and a linear map f, p after scaling f satisfies a simple multiplicative rule with norms.

Русский

Для семинормы p на E2 и линейного отображения f выполняется простое правило умножения норм на норму коэффициента.

LaTeX

$$$p(c \cdot f) = \|c\| \; p(f)$$$

Lean4

theorem comp_smul_apply (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) (x : E) : p.comp (c • f) x = ‖c‖ * p (f x) :=
  map_smul_eq_mul p _ _

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