isFiniteMeasure_sub

Mathlib.MeasureTheory.Measure.Sub

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

English

If μ is finite, then μ − ν is finite.

Русский

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

LaTeX

$$$[IsFiniteMeasure \\\\mu] \\\\Rightarrow \\\\text{IsFiniteMeasure } (\\\\mu - \\\\nu)$$$

Lean4

instance isFiniteMeasure_sub [IsFiniteMeasure μ] : IsFiniteMeasure (μ - ν) :=
  isFiniteMeasure_of_le μ sub_le

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

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

Разделы

Аффилиация

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