measure_compl_nullSet

Mathlib.MeasureTheory.Measure.MutuallySingular

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

← MathLib Explorer

English

If μ ⟂ₘ ν, then ν(h.nullSetᶜ) = 0.

Русский

Если μ ⟂ₘ ν, то ν(h.nullSetᶜ) = 0.

LaTeX

$$$\nu(h.nullSet^c) = 0$$$

Lean4

@[simp]
theorem measure_compl_nullSet (h : μ ⟂ₘ ν) : ν h.nullSetᶜ = 0 :=
  h.choose_spec.2.2
    -- TODO: this is proved by simp, but is not simplified in other contexts without the @[simp]
    -- attribute. Also, the linter does not complain about that attribute.

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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