ae_sum_eq — Mathlib

English

For Countable ι, almost-everywhere equality with respect to the sum equals the iSup of almost-everywhere equalities of the components.

Русский

Для счётного ι почти везде равенство по сумме эквивалентно наибольшему верхнему пределу почти везде для компонент.

LaTeX

$$$ \text{ae}(\sum μ) = \big( \iSup i, \text{ae}(μ_i) \big) $$$

Lean4

@[simp]
theorem ae_sum_eq [Countable ι] (μ : ι → Measure α) : ae (sum μ) = ⨆ i, ae (μ i) :=
  Filter.ext fun _ => ae_sum_iff.trans mem_iSup.symm

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