measurable_of_Iio — Mathlib

English

If a function f has measurable preimages of all intervals (-∞, x) then f is measurable.

Русский

Если прообраза каждого интервала (-∞, x) измеримы, то функция измерима.

LaTeX

$$$\forall x,\ MeasurableSet(f^{-1}(IIO(x))) \Rightarrow \ Measurable(f)$$$

Lean4

theorem measurable_of_Iio {f : δ → α} (hf : ∀ x, MeasurableSet (f ⁻¹' Iio x)) : Measurable f :=
  by
  convert measurable_generateFrom (α := δ) _
  · exact BorelSpace.measurable_eq.trans (borel_eq_generateFrom_Iio _)
  · rintro _ ⟨x, rfl⟩; exact hf x

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