ae_comp_of_ae_ae — Mathlib

English

If hp is measurable and h describes a.e.-compatibility on κ, then the a.e. property transfers to μ.bind κ.

Русский

Если hp измеримо и h задаёт ae-совместимость по κ, тогда свойство a.e. переносится на μ.bind κ.

LaTeX

$$ae_comp_of_ae_ae hp h$$

Lean4

theorem ae_comp_of_ae_ae {p : β → Prop} (hp : MeasurableSet {z | p z}) (h : ∀ᵐ y ∂μ, ∀ᵐ z ∂κ y, p z) :
    ∀ᵐ z ∂(κ ∘ₘ μ), p z := by
  rw [comp_eq_comp_const_apply]
  exact Kernel.ae_comp_of_ae_ae hp h

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