measurable_charFun — Mathlib

English

For a finite measure μ on ℝ, the function χ_μ is interval-integrable with respect to the usual volume measure on a ≤ t ≤ b.

Русский

Для конечной меры μ на ℝ функция χ_μ интегрируема на любом отрезке по обычной мере объема.

LaTeX

$$$$\\text{IntervalIntegrable}(\\chi_{\\mu}, \\text{volume}, a, b).$$$$

Lean4

@[fun_prop, measurability]
theorem measurable_charFun [OpensMeasurableSpace E] [SecondCountableTopology E] [SFinite μ] : Measurable (charFun μ) :=
  stronglyMeasurable_charFun.measurable

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