isFiniteMeasureOfIsEmpty

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

English

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

Русский

Если μ конечна, то μ.restrict s конечна для любого s.

LaTeX

$$IsFiniteMeasure(μ.restrict s)$$

Lean4

instance (priority := 50) isFiniteMeasureOfIsEmpty [IsEmpty α] : IsFiniteMeasure μ :=
  by
  rw [eq_zero_of_isEmpty μ]
  infer_instance

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

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

Разделы

Аффилиация

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