measurable_of_isClosed — Mathlib

English

If f^{-1}(s) is measurable for every closed set s, then f is measurable.

Русский

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

LaTeX

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

Lean4

theorem measurable_of_isClosed {f : δ → γ} (hf : ∀ s, IsClosed s → MeasurableSet (f ⁻¹' s)) : Measurable f :=
  by
  apply measurable_of_isOpen; intro s hs
  rw [← MeasurableSet.compl_iff, ← preimage_compl]; apply hf; rw [isClosed_compl_iff]; exact hs

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