isFiniteMeasureAdd

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

← MathLib Explorer

English

For finite μ and finite set s, μ s < ∞.

Русский

Для конечной μ и конечного множества s, μ(s) < ∞.

LaTeX

$$μ s < ∞$$

Lean4

instance isFiniteMeasureAdd [IsFiniteMeasure μ] [IsFiniteMeasure ν] : IsFiniteMeasure (μ + ν) where
  measure_univ_lt_top := by
    rw [Measure.coe_add, Pi.add_apply, ENNReal.add_lt_top]
    exact ⟨measure_lt_top _ _, measure_lt_top _ _⟩

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

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

Разделы

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

Аффилиация

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