stronglyMeasurable_charFun — Mathlib

English

The map t ↦ χ_μ(t) is strongly measurable under standard hypotheses (OpensMeasurableSpace, SecondCountableTopology, SFinite μ).

Русский

Отображение t ↦ χ_μ(t) является сильно измеримым при стандартных условиях (OpensMeasurableSpace, SecondCountableTopology, SFinite μ).

LaTeX

$$$$\\text{StronglyMeasurable}(\\chi_{\\mu}).$$$$

Lean4

@[fun_prop, measurability]
theorem stronglyMeasurable_charFun [OpensMeasurableSpace E] [SecondCountableTopology E] [SFinite μ] :
    StronglyMeasurable (charFun μ) :=
  (Measurable.stronglyMeasurable (by fun_prop)).integral_prod_left

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