measurableSet

Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEFinStronglyMeasurable.measurableSet

English

For any AEFinStronglyMeasurable f, the set sigmaFiniteSet(f) is measurable.

Русский

Для любой AEFinStronglyMeasurable f множество sigmaFiniteSet(f) измеримо.

LaTeX

$$$\\text{MeasurableSet}(\\sigmaFiniteSet(f))$$$

Lean4

protected theorem measurableSet (hf : AEFinStronglyMeasurable f μ) : MeasurableSet hf.sigmaFiniteSet :=
  hf.exists_set_sigmaFinite.choose_spec.1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru