ae_sum_iff' — Mathlib

English

If the set {x | p(x)} is measurable, then ae equality for the sum is equivalent to ae equality for each μ_i.

Русский

Если множество {x | p(x)} измеримо, то эквивалентность почти везде для суммы эквивалентна эквивалентности почти везде для каждого μ_i.

LaTeX

$$$ (\text{measurable } \{x \mid p(x)\}) \Rightarrow ( (∀ᵐ x ∂(\sum μ), p x) \iff (∀ i, ∀ᵐ x ∂μ_i, p x) ) $$$

Lean4

theorem ae_sum_iff' {μ : ι → Measure α} {p : α → Prop} (h : MeasurableSet {x | p x}) :
    (∀ᵐ x ∂sum μ, p x) ↔ ∀ i, ∀ᵐ x ∂μ i, p x :=
  sum_apply_eq_zero' h.compl

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