instIsFiniteMeasureSumOfFinite

Mathlib.MeasureTheory.Measure.Typeclasses.Finite

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

← MathLib Explorer

English

If ι is finite and μ_i are finite measures, then the sum ∑_{i∈ι} μ_i is a finite measure.

Русский

Если ι конечен и μ_i конечны, то ∑_{i∈ι} μ_i — конечная мера.

LaTeX

$$IsFiniteMeasure (∑ i ∈ univ, μ i)$$

Lean4

instance [Finite ι] {μ : ι → Measure α} [∀ i, IsFiniteMeasure (μ i)] : IsFiniteMeasure (.sum μ) where
  measure_univ_lt_top := by
    cases nonempty_fintype ι
    simp [measure_lt_top]

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

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

Разделы

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

Аффилиация

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