intervalIntegrable_charFun — Mathlib

English

If χ_μ = χ_ν as functions, then μ = ν for appropriate complete, second-countable spaces with finite measures.

Русский

Если χ_μ = χ_ν как функции, то μ = ν в подходящих полнообразных вторичносчётных пространствах с конечными мерами.

LaTeX

$$$$\\chi_{\\mu} = \\chi_{\\nu} \\Rightarrow \\mu = \\nu.$$$$

Lean4

theorem intervalIntegrable_charFun {μ : Measure ℝ} [IsFiniteMeasure μ] {a b : ℝ} :
    IntervalIntegrable (charFun μ) volume a b :=
  IntervalIntegrable.mono_fun' (g := fun _ ↦ μ.real Set.univ) (by simp) stronglyMeasurable_charFun.aestronglyMeasurable
    (ae_of_all _ norm_charFun_le)

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