instMeasurableConstSMul — Mathlib

English

There is a measurability transfer to the opposite scalar action: if the left action is measurable, the right action by Mᵐᵒᵖ is measurable under centrality.

Русский

При условии центральности переносится измеримость левого действия на правое действие Mᵐᵒᵖ.

LaTeX

$$$\text{MeasurableConstSMul}(M^{op}, \alpha)$$$

Lean4

/-- If a scalar is central, then its right action is measurable when its left action is. -/
@[to_additive]
nonrec instance instMeasurableConstSMul [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] [MeasurableConstSMul M α] :
    MeasurableConstSMul Mᵐᵒᵖ α where measurable_const_smul := by simpa using measurable_const_smul

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