English
Let G be a group with a measurable division operation and let f, g: α → G be almost everywhere μ-measurable. Then the pointwise quotient a ↦ f(a) / g(a) is also almost everywhere μ-measurable.
Русский
Пусть G — группа с измеримой операцией деления. Пусть f, g: α → G измеримы почти всюду относительно меры μ. Тогда функция a ↦ f(a) / g(a) измерима почти всюду.
LaTeX
$$$AEMeasurable\ f\ \mu \land AEMeasurable\ g\ \mu \\Rightarrow AEMeasurable\\ (fun a \\mapsto f\\ a / g\\ a)\\ \mu$$$
Lean4
@[to_additive (attr := fun_prop, aesop safe 20 apply (rule_sets := [Measurable]))]
theorem div' [MeasurableDiv₂ G] (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) : AEMeasurable (f / g) μ :=
measurable_div.comp_aemeasurable (hf.prodMk hg)
