eq_zero_of_absolutelyContinuous_of_mutuallySingular

Mathlib.MeasureTheory.Measure.MutuallySingular

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

Lean4

theorem eq_zero_of_absolutelyContinuous_of_mutuallySingular {μ ν : Measure α} (h_ac : μ ≪ ν) (h_ms : μ ⟂ₘ ν) : μ = 0 :=
  by
  rw [← Measure.MutuallySingular.self_iff]
  exact h_ms.mono_ac Measure.AbsolutelyContinuous.rfl h_ac

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

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

Разделы

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

Аффилиация

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