singularPart_zero_right

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

English

For any μ, μ.singularPart 0 = μ.

Русский

Для любой μ имеет место μ.singularPart 0 = μ.

LaTeX

$$$$ μ.singularPart 0 = μ $$$$

Lean4

@[simp]
theorem singularPart_zero_right (μ : Measure α) : μ.singularPart 0 = μ :=
  by
  conv_rhs => rw [haveLebesgueDecomposition_add μ 0]
  simp

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

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

Разделы

Аффилиация

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