ae_ae_of_ae_bind — Mathlib

English

If f is AEMeasurable and h holds almost everywhere for m.bind f, then a.e. b under f implies a.e. under bind f.

Русский

Если f — AEMeasurable и свойство выполняется почти наверняка для m.bind f, то почти наверняка относительно a и b

LaTeX

$$ae_ae_of_ae_bind: (hf : AEMeasurable f m) (h : ∀ᵐ b ∂m.bind f, p b) → ∀ᵐ a ∂m, ∀ᵐ b ∂f a, p b$$

Lean4

theorem ae_ae_of_ae_bind {m : Measure α} {f : α → Measure β} {p : β → Prop} (hf : AEMeasurable f m)
    (h : ∀ᵐ b ∂m.bind f, p b) : ∀ᵐ a ∂m, ∀ᵐ b ∂f a, p b :=
  ae_of_ae_map hf <| ae_ae_of_ae_join h

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