smul_comp — Mathlib

English

For a fixed linear map f, the map p ↦ p ∘ f is an AddMonoidHom from Seminorm 𝕜₂ E₂ to Seminorm 𝕜 E.

Русский

Для данного отображения f отображение p ↦ p ∘ f является гомоморфизмом аддитивных моноидов между полунормами.

LaTeX

$$$ pullback_f: Seminorm 𝕜₂ E₂ \to+ Seminorm 𝕜 E \quad\text{defined by}\quad p \mapsto p \circ f $$$

Lean4

theorem smul_comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : R) : (c • p).comp f = c • p.comp f :=
  ext fun _ => rfl

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