measurableSet_integrable — Mathlib

English

If f is a function of two variables with appropriate measurability, the set of x for which f(x) is integrable with respect to ν is measurable.

Русский

Множество x, для которого f(x) интегрируемо по ν, является измеримым.

LaTeX

$$$$\\text{MeasurableSet}\\{x \\mid \\operatorname{Integrable}(f(x), \\nu)\\}$$$$

Lean4

theorem measurableSet_integrable [SFinite ν] ⦃f : α → β → E⦄ (hf : StronglyMeasurable (uncurry f)) :
    MeasurableSet {x | Integrable (f x) ν} :=
  by
  simp_rw [Integrable, hf.of_uncurry_left.aestronglyMeasurable, true_and]
  exact measurableSet_lt (Measurable.lintegral_prod_right hf.enorm) measurable_const

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