div — Mathlib

English

If f,g: α → G are almost everywhere μ-measurable and G has a measurable division, then the function a ↦ f(a) / g(a) is almost everywhere μ-measurable.

Русский

Если f, g: α → G измеримы почти всюду по μ и в G задано измеримое деление, то функция a ↦ f(a) / g(a) измерима почти всюду по μ.

LaTeX

$$$AEMeasurable\\ f\\ \\,\\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 (fun a => f a / g a) μ :=
  measurable_div.comp_aemeasurable (hf.prodMk hg)

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