div_const — Mathlib

English

If f is measurable, then x ↦ f(x) / c is measurable for fixed c.

Русский

Если f измеримо, то x ↦ f(x) / c измеримо для фиксированного c.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow \\text{Measurable}(x \\mapsto f(x) / c).$$$

Lean4

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

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