singularPart_le

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

← MathLib Explorer

English

μ.singularPart ν ≤ μ.

Русский

μ.singularPart ν не превосходит μ.

LaTeX

$$μ.singularPart ν ≤ μ$$

Lean4

theorem singularPart_le (μ ν : Measure α) : μ.singularPart ν ≤ μ :=
  by
  by_cases hl : HaveLebesgueDecomposition μ ν
  · conv_rhs => rw [haveLebesgueDecomposition_add μ ν]
    exact Measure.le_add_right le_rfl
  · rw [singularPart, dif_neg hl]
    exact Measure.zero_le μ

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

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

Разделы

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

Аффилиация

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