instIsFiniteMeasure

Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue

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

English

If μ is finite, then μ.singularPart ν is finite as well.

Русский

Если μ конечна, то μ.singularPart ν также конечна.

LaTeX

$$$$ [IsFiniteMeasure μ] \Rightarrow IsFiniteMeasure(μ.singularPart ν) $$$$

Lean4

instance instIsFiniteMeasure [IsFiniteMeasure μ] : IsFiniteMeasure (μ.singularPart ν) :=
  isFiniteMeasure_of_le μ <| singularPart_le μ ν

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

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

Разделы

Аффилиация

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