ae_ae_of_ae_compProd — Mathlib

English

If almost everywhere in μ ⊗ₘ κ, p holds, then almost everywhere in μ, almost everywhere in κ a, p(a,b).

Русский

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

LaTeX

$$$[\\mathrm{SFinite}\\; μ] [\\mathrm{IsSFiniteKernel}\\; κ] \\{p : α × β \\to \\mathrm{Prop}\\} (hp : \\mathrm{MeasurableSet}\\; {x | p x}) \\Rightarrow (\\mathrm{ae}\\; μ.compProd κ)\\, p$$$

Lean4

theorem ae_ae_of_ae_compProd [SFinite μ] [IsSFiniteKernel κ] {p : α × β → Prop} (h : ∀ᵐ x ∂(μ ⊗ₘ κ), p x) :
    ∀ᵐ a ∂μ, ∀ᵐ b ∂κ a, p (a, b) := by convert Kernel.ae_ae_of_ae_compProd h

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