ae_sum_iff — Mathlib

English

For Countable ι, almost-everywhere equality with respect to the sum μ is equivalent to almost-everywhere equality for every μ_i.

Русский

Для счетного множества индексов ι, почти везде по мере суммы выполняется эквивалентность по каждой μ_i.

LaTeX

$$$ (∀ᵐ x ∂(\sum μ), p x) \iff (∀ i, ∀ᵐ x ∂μ_i, p x) $$$

Lean4

theorem ae_sum_iff [Countable ι] {μ : ι → Measure α} {p : α → Prop} : (∀ᵐ x ∂sum μ, p x) ↔ ∀ i, ∀ᵐ x ∂μ i, p x :=
  sum_apply_eq_zero

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