English
Equipping Units M with a measurable space via comap ensures compatibility with the val map.
Русский
Единицы M оснащаются измеримым пространством через комап-переменную val совместимо с отображением val.
LaTeX
$$$\\text{MeasurableSpace}(M^{\\times}) = \\text{MeasurableSpace.comap}(\\mathrm{val},\\, \\text{MeasurableSpace}(M))$$$
Lean4
/-- If a scalar is central, then its right action is measurable when its left action is. -/
nonrec instance op {M α} [MeasurableSpace M] [MeasurableSpace α] [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α]
[MeasurableSMul₂ M α] : MeasurableSMul₂ Mᵐᵒᵖ α :=
⟨show Measurable fun x : Mᵐᵒᵖ × α => op (unop x.1) • x.2
by
simp_rw [op_smul_eq_smul]
exact (measurable_mul_unop.comp measurable_fst).smul measurable_snd⟩
