measurableSet_integrable — Mathlib

English

If f is measurable, then the set of x for which the kernel-integral of f with respect to κ x is integrable is measurable.

Русский

Если f измеримо, то множество x, для которого интеграл по ядру κ x сходится, измеримо.

LaTeX

$$$\\{x : \\alpha : \\} \\;\\text{ : } \\text{Integrable}(f, \\kappa x) \\text{ is measurable}$$$

Lean4

theorem measurableSet_integrable ⦃f : β → E⦄ (hf : StronglyMeasurable f) : MeasurableSet {a | Integrable f (κ a)} :=
  by
  simp_rw [Integrable, hf.aestronglyMeasurable, true_and]
  exact measurableSet_lt hf.enorm.lintegral_kernel measurable_const

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