of_trim — Mathlib

English

If f is AEStronglyMeasurable with μ.trim hm₀, then it is AEStronglyMeasurable with μ.

Русский

Если f AE‑строго измерима по μ.trim hm₀, то по μ тоже AE‑строго измерима.

LaTeX

$$$AEStronglyMeasurable_m(f, μ.trim hm₀) \\Rightarrow AEStronglyMeasurable_m(f, μ)$$$

Lean4

theorem of_trim {m₀' : MeasurableSpace α} (hm₀ : m₀' ≤ m₀) (hf : AEStronglyMeasurable[m] f (μ.trim hm₀)) :
    AEStronglyMeasurable[m] f μ := by obtain ⟨g, hg_meas, hfg⟩ := hf; exact ⟨g, hg_meas, ae_eq_of_ae_eq_trim hfg⟩

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