isFiniteMeasure_restrict

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

URI: https://scilib.ai/kg/mathlib#MeasureTheory.isFiniteMeasure_restrict

English

If μ is finite, then μ.restrict s is finite for any measurable s.

Русский

Если μ конечна, то ограничение μ на any измеримое s также конечно.

LaTeX

$$$IsFiniteMeasure(\\mu)\\Rightarrow IsFiniteMeasure(\\mu\\restriction s)$$$

Lean4

theorem isFiniteMeasure_restrict : IsFiniteMeasure (μ.restrict s) ↔ μ s ≠ ∞ := by
  simp [isFiniteMeasure_iff, lt_top_iff_ne_top]

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

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

Разделы

Аффилиация

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