measurableSet_of_null

Mathlib.MeasureTheory.Measure.NullMeasurable

URI: https://scilib.ai/kg/mathlib#MeasureTheory.measurableSet_of_null

English

If μ is complete and μ s = 0, then s is measurable.

Русский

Если μ полна и μ(s)=0, то s измеримо.

LaTeX

$$$[\mu.IsComplete] (\mu s = 0) \Rightarrow \mathrm{MeasurableSet}(s).$$$

Lean4

theorem measurableSet_of_null [μ.IsComplete] (hs : μ s = 0) : MeasurableSet s :=
  MeasureTheory.Measure.IsComplete.out' s hs

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

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

Разделы

Аффилиация

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