ae_prod_iff_ae_ae — Mathlib

English

For a predicate p on α × β with measurable set {x | p x} measurable, the statement μ × ν-ae implies that p holds almost everywhere in the product iff p holds almost everywhere in each fiber.

Русский

Для предиката p на α × β с измеримой подстановкой, равенство почти наверняка в произведении эквивалентно тому, что p выполняется почти наверняка по каждому срезу.

LaTeX

$$$\text{MeasurableSet} \{x\mid p(x)\} \Rightarrow (∀^{\!} z ∂μ.prod ν, p z) \iff (∀^{\!} x ∂μ, ∀^{\!} y ∂ν, p(x,y))$$$

Lean4

theorem ae_prod_iff_ae_ae {p : α × β → Prop} (hp : MeasurableSet {x | p x}) :
    (∀ᵐ z ∂μ.prod ν, p z) ↔ ∀ᵐ x ∂μ, ∀ᵐ y ∂ν, p (x, y) :=
  measure_prod_null hp.compl

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