English
The composition of a seminorm with a linear map is again a seminorm, defined by (p ∘ f)(x) = p(f(x)).
Русский
Состав полунормы с линейным отображением снова является полунормой, задаваемой (p ∘ f)(x) = p(f(x)).
LaTeX
$$$ (p \circ f)(x) = p(f(x)) $$$
Lean4
/-- Composition of a seminorm with a linear map is a seminorm. -/
def comp (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) : Seminorm 𝕜 E :=
{
p.toAddGroupSeminorm.comp f.toAddMonoidHom with
toFun := fun x =>
p
(f x)
-- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to change `map_smulₛₗ` to `map_smulₛₗ _`
smul' _ _ := by simp only [map_smulₛₗ _, map_smul_eq_mul, RingHomIsometric.norm_map] }
