measurable_of_isOpen — Mathlib

English

If f is such that f^{-1}(U) is measurable for every open set U, then f is measurable.

Русский

Если для каждого открытого множества U выполняется, что обратное изображение f^{-1}(U) измеримо, то функция f измерима.

LaTeX

$$$\\Big( \\forall U, \\text{IsOpen}(U) \\Rightarrow \\text{MeasurableSet}(f^{-1}(U)) \\Big) \\Rightarrow \\text{Measurable}(f).$$$

Lean4

theorem measurable_of_isOpen {f : δ → γ} (hf : ∀ s, IsOpen s → MeasurableSet (f ⁻¹' s)) : Measurable f :=
  by
  rw [‹BorelSpace γ›.measurable_eq]
  exact measurable_generateFrom hf

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