instSMulCommClass — Mathlib

English

If scalars from R and R' act commuting on ENNReal, then they also commute on measures with the defined action: c • (d • μ) = d • (c • μ).

Русский

Если действия скаляров из R и R' на ENNReal коммутируют, то они коммутируют и на мерах: c • (d • μ) = d • (c • μ).

LaTeX

$$$\forall \mu:\text{Measure}(\alpha), \forall c:\, R, \forall d:\, R',\; c \cdot (d \cdot \mu) = d \cdot (c \cdot \mu).$$$

Lean4

instance instSMulCommClass [SMulCommClass R R' ℝ≥0∞] {_ : MeasurableSpace α} : SMulCommClass R R' (Measure α) :=
  ⟨fun _ _ _ => ext fun _ _ => smul_comm _ _ _⟩

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