smul_apply — Mathlib

English

Applying a scalar to a seminorm and evaluating at x is the same as applying the scalar to the value p(x).

Русский

Применение скаляра к семинорме и вычисление в точке x эквивалентно применению скаляра к значению p(x).

LaTeX

$$$ (r \cdot p)(x) = r \cdot p(x) $$$

Lean4

@[simp]
theorem smul_apply [SMul R ℝ] [SMul R ℝ≥0] [IsScalarTower R ℝ≥0 ℝ] (r : R) (p : Seminorm 𝕜 E) (x : E) :
    (r • p) x = r • p x :=
  rfl

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