instSMulCommClass — Mathlib

English

There exists a compatibility class of scalar actions: if the scalar actions on ENNReal satisfy the usual commutativity conditions, then they commute when acting on outer measures as well.

Русский

Существует класс совместимости скалярных действий: если скалярные действия на ENNReal удовлетворяют условиям коммутативности, то они коммутируют и при действии на внешние меры.

LaTeX

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

Lean4

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

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