mono — Mathlib

English

If a function is strongly measurable with respect to a coarser σ-algebra m' and m' ≤ m, it is strongly measurable with respect to m.

Русский

Если функция сильно измерима относительно более грубой σ-алгебры m' и m' ⊆ m, то она сильно измерима относительно m.

LaTeX

$$$\text{StronglyMeasurable}_{m'}(f) \land m' \le m \Rightarrow \text{StronglyMeasurable}_{m}(f)$$$

Lean4

protected theorem mono {m m' : MeasurableSpace α} [TopologicalSpace β] (hf : StronglyMeasurable[m'] f)
    (h_mono : m' ≤ m) : StronglyMeasurable[m] f :=
  by
  let f_approx : ℕ → @SimpleFunc α m β := fun n =>
    @SimpleFunc.mk α m β (hf.approx n) (fun x => h_mono _ (SimpleFunc.measurableSet_fiber' _ x))
      (SimpleFunc.finite_range (hf.approx n))
  exact ⟨f_approx, hf.tendsto_approx⟩

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