smul_apply — Mathlib

English

The coercion of the zero seminorm yields the zero function: for all x, (0 : NonarchAddGroupSeminorm E) x = 0.

Русский

Приведение нулевого семинорма даёт нулевую функцию: для всех x, (0 : NonarchAddGroupSeminorm E) x = 0.

LaTeX

$$$ \forall x : E,\; (0 : \mathrm{NonarchAddGroupSeminorm} E)(x) = 0 $$$

Lean4

@[simp]
theorem smul_apply (r : R) (p : NonarchAddGroupSeminorm E) (x : E) : (r • p) x = r • p x :=
  rfl

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