measurableSet_nullSet

Mathlib.MeasureTheory.Measure.MutuallySingular

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet

English

If μ ⟂ₘ ν, then h.nullSet is measurable.

Русский

Если μ ⟂ₘ ν, то h.nullSet измеримо.

LaTeX

$$$\mathrm{MeasurableSet}\ h.nullSet$$$

Lean4

theorem measurableSet_nullSet (h : μ ⟂ₘ ν) : MeasurableSet h.nullSet :=
  h.choose_spec.1

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

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

Разделы

Аффилиация

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