smul_apply — Mathlib

English

The application of a scalar to an outer measure respects pointwise evaluation: (c • m)(s) = c • m(s).

Русский

Применение скаляра к внешней мере сохраняет точечную оценку: (c • m)(s) = c • m(s).

LaTeX

$$$\forall c:\, R,\forall m:\, OuterMeasure\ \alpha,\forall s:\, Set\ \alpha,\ (c \cdot m)\,s = c \cdot (m\,s).$$$

Lean4

theorem smul_apply (c : R) (m : OuterMeasure α) (s : Set α) : (c • m) s = c • m s :=
  rfl

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