English
For a group with a division structure, the map h ↦ h / g is measurable when g is fixed.
Русский
Если фиксировано g, то карта h ↦ h / g измерима в группе с делением.
LaTeX
$$$\\text{Measurable}(h \\mapsto h / g)\\;\\text{ for fixed } g.$$$
Lean4
/-- A version of `measurable_div_const` that assumes `MeasurableMul` instead of
`MeasurableDiv`. This can be nice to avoid unnecessary type-class assumptions. -/
@[to_additive /-- A version of `measurable_sub_const` that assumes `MeasurableAdd` instead of
`MeasurableSub`. This can be nice to avoid unnecessary type-class assumptions. -/
]
theorem measurable_div_const' {G : Type*} [DivInvMonoid G] [MeasurableSpace G] [MeasurableMul G] (g : G) :
Measurable fun h => h / g := by simp_rw [div_eq_mul_inv, measurable_mul_const]
