English
If a property p holds μ-almost everywhere, then for any scalar c, p also holds c•μ-almost everywhere.
Русский
Если свойство p верно μ-почти везде, то при любом скаляре c также верно, что p выполняется почти повсеместно для c•μ.
LaTeX
$$$\forall p,\; (\forall^\text{a} x \; p(x)\; [\mu]) \Rightarrow (\forall^\text{a} x \; p(x)\; [c\cdot\mu]).$$$
Lean4
instance instDistribMulAction [Monoid R] [DistribMulAction R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] {_ : MeasurableSpace α} :
DistribMulAction R (Measure α) :=
Injective.distribMulAction ⟨⟨toOuterMeasure, zero_toOuterMeasure⟩, add_toOuterMeasure⟩ toOuterMeasure_injective
smul_toOuterMeasure