instMulAction — Mathlib

English

Outer measures carry a scalar action of a monoid: for c in R and m an outer measure, c • m is again an outer measure, defined by (c • m)(s) = c • m(s).

Русский

Внешние меры имеют действие умножения на моноид: для элемента c и внешней меры m получаем новую внешнюю меру c • m, определяемую (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

instance instMulAction {R : Type*} [Monoid R] [MulAction R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] :
    MulAction R (OuterMeasure α) :=
  Injective.mulAction _ coe_fn_injective coe_smul

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