measurableSet_isFiniteMeasure — Mathlib

English

The set of all finite measures on Ω is a measurable subset of the space of all measures on Ω (in the Giry monad sense).

Русский

Множество всех конечных мер на Ω является измеримым подмножеством пространства всех мер на Ω (в смысле монадного Гири).

LaTeX

$$$\\{\\mu \\in \\mathrm{Measure}(\\Omega) \\mid \\mathrm{IsFiniteMeasure}(\\mu)\\}$ is MeasurableSet$$

Lean4

/-- The set of all finite measures is a measurable set in the Giry monad. -/
theorem measurableSet_isFiniteMeasure : MeasurableSet {μ : Measure Ω | IsFiniteMeasure μ} :=
  by
  suffices {μ : Measure Ω | IsFiniteMeasure μ} = (fun μ => μ univ) ⁻¹' (Set.Ico 0 ∞)
    by
    rw [this]
    exact Measure.measurable_coe MeasurableSet.univ measurableSet_Ico
  ext μ
  simp only [mem_setOf_eq, mem_preimage, mem_Ico, zero_le, true_and]
  exact isFiniteMeasure_iff μ

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