English
If the set {x, y : p x y} is measurable, then almost everywhere in x and y can be swapped: (∀ᵐ x ∂μ, ∀ᵐ y ∂ν, p x y) ↔ (∀ᵐ y ∂ν, ∀ᵐ x ∂μ, p x y).
Русский
Если множество {x,y | p x y} измеримо, то можно поменять кванторы почти наверняка: (∀ᵐx ∂μ, ∀ᵐy ∂ν, p x y) ↔ (∀ᵐy ∂ν, ∀ᵐx ∂μ, p x y).
LaTeX
$$$\\text{MeasurableSet}(\\{(x,y)\\mid p(x,y)\\}) \\Rightarrow (\\forall^{\\ae} x \\partial μ)(\\forall^{\\ ae} y \\partial ν)(p(x,y)) \\iff (\\forall^{\\ ae} y \\partial ν)(\\forall^{\\ ae} x \\partial μ)(p(x,y))$$$
Lean4
theorem ae_ae_comm {p : α → β → Prop} (h : MeasurableSet {x : α × β | p x.1 x.2}) :
(∀ᵐ x ∂μ, ∀ᵐ y ∂ν, p x y) ↔ ∀ᵐ y ∂ν, ∀ᵐ x ∂μ, p x y :=
calc
_ ↔ ∀ᵐ x ∂μ.prod ν, p x.1 x.2 := .symm <| ae_prod_iff_ae_ae h
_ ↔ ∀ᵐ x ∂ν.prod μ, p x.2 x.1 := by rw [← prod_swap, ae_map_iff (by fun_prop) h]; simp
_ ↔ ∀ᵐ y ∂ν, ∀ᵐ x ∂μ, p x y := ae_prod_iff_ae_ae <| measurable_swap h
