measurableSMul₂_iterateMulAct — Mathlib

English

If a scalar is central, then its right action is measurable when its left action is. In particular, MeasurableConstSMul holds for Mᵐᵒᵖ on α.

Русский

Если скаляр центральный, правая акция измерима, когда левая — измерима; верно и для Mᵐᵒᵖ.

LaTeX

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

Lean4

@[to_additive]
theorem measurableSMul₂_iterateMulAct (h : Measurable f) : MeasurableSMul₂ (IterateMulAct f) α where
  measurable_smul :=
    suffices Measurable fun p : α × IterateMulAct f ↦ f^[p.2.val] p.1 from this.comp measurable_swap
    measurable_from_prod_countable_left fun n ↦ h.iterate n.val

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