isFiniteMeasure_trim

Mathlib.MeasureTheory.Measure.Trim

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

← MathLib Explorer

English

If μ is finite and hm: m ≤ m0, then μ.trim hm is finite.

Русский

Если μ конечно по мере, и hm: m ≤ m0, то μ.trim hm конечно.

LaTeX

$$$\\text{IsFiniteMeasure}(μ.trim hm).$$$

Lean4

instance isFiniteMeasure_trim (hm : m ≤ m0) [IsFiniteMeasure μ] : IsFiniteMeasure (μ.trim hm) where
  measure_univ_lt_top := by
    rw [trim_measurableSet_eq hm (@MeasurableSet.univ _ m)]
    exact measure_lt_top _ _

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

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

Разделы

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

Аффилиация

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