ae_prod_mem_iff_ae_ae_mem — Mathlib

English

For s ⊆ α×β measurable, a product-a.e. membership of z ∈ s is equivalent to the fibers having a.e. membership for almost all x and y.

Русский

Для измеримой пары множеств s ⊆ α×β эквивалентно, что z ∈ s почти наверняка по μ×ν тогда и только тогда, когда по срезам x и y зондируется множество.

LaTeX

$$$(s \subseteq α×β)$ MeasurableSet \Rightarrow (∀^{\!} z ∂μ.prod ν, z ∈ s) \iff ∀^{\!} x ∂μ, ∀^{\!} y ∂ν, (x,y) ∈ s$$$

Lean4

theorem ae_prod_mem_iff_ae_ae_mem {s : Set (α × β)} (hs : MeasurableSet s) :
    (∀ᵐ z ∂μ.prod ν, z ∈ s) ↔ ∀ᵐ x ∂μ, ∀ᵐ y ∂ν, (x, y) ∈ s :=
  measure_prod_null hs.compl

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