restrict_compl_nullSet

Mathlib.MeasureTheory.Measure.MutuallySingular

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

English

The restricted measure ν.restrict h.nullSetᶜ equals the zero measure.

Русский

Ограниченная мера ν.restrict h.nullSetᶜ равна нулевой мере.

LaTeX

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

Lean4

@[simp]
theorem restrict_compl_nullSet (h : μ ⟂ₘ ν) : ν.restrict h.nullSetᶜ = 0 := by simp

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

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

Разделы

Аффилиация

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