ae_of_bind — Mathlib

English

If hf is AEMeasurable f m and hg is AEMeasurable g (m.bind f), then ∀ᵐ a ∂m, AEMeasurable g (f a).

Русский

Если hf — AEMeasurable f m и hg — AEMeasurable g (m.bind f), то для почти наверняка по m выполняется AEMeasurable g (f a).

LaTeX

$$$\\text{AEMeasurable.ae_of_bind}: (hf: AEMeasurable f m) (hg: AEMeasurable g (m.bind f)) → ∀ᵐ a ∂m, AEMeasurable g (f a)$$$

Lean4

theorem _root_.AEMeasurable.ae_of_bind {γ : Type*} {_ : MeasurableSpace γ} {m : Measure α} {f : α → Measure β}
    {g : β → γ} (hf : AEMeasurable f m) (hg : AEMeasurable g (m.bind f)) : ∀ᵐ a ∂m, AEMeasurable g (f a) :=
  ae_of_ae_map hf hg.ae_of_join

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