instIsScalarTower — Mathlib

English

If R, R' act on ENNReal with a scalar tower, then there is an induced IsScalarTower on the measure space: (r • (r' • μ)) = (r • r') • μ.

Русский

Если существуют действия скаляров R и R' на ENNReal с торовым свойством, то на пространства мер существует соответствующее свойство: r • (r' • μ) = (r • r') • μ.

LaTeX

$$$\forall r:\, R,\forall r':\, R',\forall \mu:\; (r \cdot (r' \cdot \mu)) = (r \cdot r') \cdot \mu.$$$

Lean4

instance instIsScalarTower [SMul R R'] [IsScalarTower R R' ℝ≥0∞] {_ : MeasurableSpace α} :
    IsScalarTower R R' (Measure α) :=
  ⟨fun _ _ _ => ext fun _ _ => smul_assoc _ _ _⟩

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