isFiniteMeasureSMulNNReal

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

← MathLib Explorer

English

For finite μ, the normalized measure (μ univ)⁻¹ • μ is finite.

Русский

Для конечной μ нормализованная мера (μ(univ))⁻¹ • μ конечна.

LaTeX

$$IsFiniteMeasure ( (μ univ)⁻¹ • μ )$$

Lean4

instance isFiniteMeasureSMulNNReal [IsFiniteMeasure μ] {r : ℝ≥0} : IsFiniteMeasure (r • μ) where
  measure_univ_lt_top := ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_lt_top _ _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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