ae_of_join — Mathlib

English

If f is AEMeasurable with respect to m.join, then almost everywhere in m there is AEMeasurable f μ.

Русский

Если f AEMeasurable относительно m.join, то почти наверняка в m существует AEMeasurable f(μ).

LaTeX

$$AEMeasurable.ae_of_join: (h : AEMeasurable f m.join) ⇒ ∀ᵐ μ ∂m, AEMeasurable f μ$$

Lean4

theorem _root_.AEMeasurable.ae_of_join {m : Measure (Measure α)} {f : α → β} (h : AEMeasurable f m.join) :
    ∀ᵐ μ ∂m, AEMeasurable f μ :=
  let ⟨g, hgm, hg⟩ := h;
  (ae_ae_of_ae_join hg).mono fun _μ hμ ↦ ⟨g, hgm, hμ⟩

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