English
If a property p on α × β holds almost everywhere with respect to μ × ν, then for μ-almost every x, the function y ↦ p(x,y) holds ν-almost everywhere.
Русский
Если свойство p на α × β выполняется практически повсюду относительно μ × ν, то для почти всех x в α свойство p(x,y) выполняется почти повсюду по y относительно ν.
LaTeX
$$$ (\forall z \; p(z) \text{ for } z \sim μ \otimes ν) \Rightarrow \forall^{\!} x \partial μ, \forall^{\!} y \partial ν, p(x,y) $$$
Lean4
/-- Note: the converse is not true. For a counterexample, see
Walter Rudin *Real and Complex Analysis*, example (c) in section 8.9. It is true if the set is
measurable, see `ae_prod_mem_iff_ae_ae_mem`. -/
theorem ae_ae_of_ae_prod {p : α × β → Prop} (h : ∀ᵐ z ∂μ.prod ν, p z) : ∀ᵐ x ∂μ, ∀ᵐ y ∂ν, p (x, y) :=
measure_ae_null_of_prod_null h
