ae_add_measure_iff — Mathlib

English

For measures μ and ν, an event holds almost everywhere under μ+ν if and only if it holds almost everywhere under μ and under ν separately.

Русский

Для мер μ и ν событие выполняется почти всюду под суммарной мерой μ+ν тогда и только тогда, когда оно выполняется почти всюду отдельно по μ и по ν.

LaTeX

$$$(\forall^\mathrm{a.e.}_{x} p(x) \text{ w.r.t. } μ + ν) \iff (\forall^\mathrm{a.e.}_{x} p(x) \text{ w.r.t. } μ) \land (\forall^\mathrm{a.e.}_{x} p(x) \text{ w.r.t. } ν).$$$

Lean4

theorem ae_add_measure_iff {p : α → Prop} {ν} : (∀ᵐ x ∂μ + ν, p x) ↔ (∀ᵐ x ∂μ, p x) ∧ ∀ᵐ x ∂ν, p x :=
  add_eq_zero

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