ae_compProd_iff — Mathlib

English

For SFinite μ and IsSFiniteKernel κ, the property p holds almost everywhere on μ ⊗ₘ κ iff p(a,b) holds almost everywhere with respect to μ and κ a.

Русский

Для SFinite μ и IsSFiniteKernel κ: p почти всюду на μ ⊗ₘ κ тогда и только тогда, когда p(a,b) почти всюду по μ и κ a.

LaTeX

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

Lean4

theorem ae_compProd_iff [SFinite μ] [IsSFiniteKernel κ] {p : α × β → Prop} (hp : MeasurableSet {x | p x}) :
    (∀ᵐ x ∂(μ ⊗ₘ κ), p x) ↔ ∀ᵐ a ∂μ, ∀ᵐ b ∂(κ a), p (a, b) :=
  Kernel.ae_compProd_iff hp

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