const_div — Mathlib

English

If f is almost everywhere measurable, then x ↦ c / f(x) is almost everywhere measurable.

Русский

Если f измеримо почти всюду, то x ↦ c / f(x) измеримо почти всюду.

LaTeX

$$$\\text{AEMeasurable}(f) \\Rightarrow \\forall c, \\; \\text{AEMeasurable}(x \\mapsto c / f(x)).$$$

Lean4

@[to_additive (attr := fun_prop, measurability)]
theorem const_div [MeasurableDiv G] (hf : AEMeasurable f μ) (c : G) : AEMeasurable (fun x => c / f x) μ :=
  (MeasurableDiv.measurable_const_div c).comp_aemeasurable hf

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