instDistribMulAction — Mathlib

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

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