nullSet

Mathlib.MeasureTheory.Measure.MutuallySingular

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

English

If μ ⟂ₘ ν, then the nullSet is a measurable set.

Русский

Если μ ⟂ₘ ν, то нулевое множество является измеримой множеством.

LaTeX

$$"MeasurableSet" h.nullSet$$

Lean4

/-- A set such that `μ h.nullSet = 0` and `ν h.nullSetᶜ = 0`. -/
def nullSet (h : μ ⟂ₘ ν) : Set α :=
  h.choose

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

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

Разделы

Аффилиация

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