comp_smul — Mathlib

English

If p,q are seminorms, then (p ⊓ q) applied to x equals the infimum of p(u) + q(x-u) over u.

Русский

Если p,q — семинормы, то (p ⊓ q)(x) = inf_u [ p(u) + q(x-u) ].

LaTeX

$$$(p \inf q)(x) = \inf_{u \in E} \left( p(u) + q(x-u) \right)$$$

Lean4

theorem comp_smul (p : Seminorm 𝕜₂ E₂) (f : E →ₛₗ[σ₁₂] E₂) (c : 𝕜₂) : p.comp (c • f) = ‖c‖₊ • p.comp f :=
  ext fun _ => by
    rw [comp_apply, smul_apply, LinearMap.smul_apply, map_smul_eq_mul, NNReal.smul_def, coe_nnnorm, smul_eq_mul,
      comp_apply]

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