instIsScalarTower — Mathlib

English

There is a scalar tower structure on OuterMeasure: if R, R' act on ENNReal with appropriate towers, then IsScalarTower R R' (OuterMeasure α).

Русский

Существует структура стека скаляров на OuterMeasure: если R и R' действуют над ENNReal и между ними корректна связка, то IsScalarTower R R' (OuterMeasure α).

LaTeX

$$$\text{IsScalarTower } R R' (OuterMeasure\, \alpha).$$$

Lean4

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

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