instIsFiniteMeasureSumMeasure — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance {s : Finset ι} {μ : ι → Measure α} [∀ i, IsFiniteMeasure (μ i)] : IsFiniteMeasure (∑ i ∈ s, μ i) where
  measure_univ_lt_top := by simp [measure_lt_top]

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