div_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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