ae_compProd_of_ae_ae — Mathlib

English

If p holds almost everywhere on μ ⊗ₘ κ, then p(a,b) holds almost everywhere with respect to κ a for μ-almost every a.

Русский

Если свойство p выполняется почти всюду по μ ⊗ₘ κ, то почти всюду по a в μ выполнено p(a,b) для κ a-почти для a.

LaTeX

$$$[\\mathrm{SFinite}\\; μ] [\\mathrm{IsSFiniteKernel}\\; κ] \\{p : \\mathrm{Prod}\\; α β \\to \\mathrm{Prop}\\} (hp : \\mathrm{MeasurableSet}\\; {x | p x}) \\Rightarrow (∀ᵐ x ∂(μ \\otimes_m κ), p x) \\Rightarrow (∀ᵐ a ∂μ, ∀ᵐ b ∂κ a, p (a, b))$$

Lean4

theorem ae_compProd_of_ae_ae {p : α × β → Prop} (hp : MeasurableSet {x | p x}) (h : ∀ᵐ a ∂μ, ∀ᵐ b ∂(κ a), p (a, b)) :
    ∀ᵐ x ∂(μ ⊗ₘ κ), p x :=
  Kernel.ae_compProd_of_ae_ae hp h

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