mono — Mathlib

English

If m ≤ m' and f is AEStronglyMeasurable f μ, then AEStronglyMeasurable f μ under the larger σ-algebra.

Русский

Если m ≤ m' и f AE‑строго измерима по μ, то AE‑строго измерима по более крупной сигма‑алгебре.

LaTeX

$$$\\text{MeasurableSpace}_{\\le}(m, m') \\Rightarrow AEStronglyMeasurable_m(f, μ) \\Rightarrow AEStronglyMeasurable_m(f, μ)$$$

Lean4

theorem mono {m'} (hm : m ≤ m') (hf : AEStronglyMeasurable[m] f μ) : AEStronglyMeasurable[m'] f μ :=
  let ⟨f', hf'_meas, hff'⟩ := hf;
  ⟨f', hf'_meas.mono hm, hff'⟩

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