measurable_of_isClosed' — Mathlib

English

If for all closed s with s nonempty and s ≠ the whole space, f^{-1}(s) is measurable, then f is measurable.

Русский

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

LaTeX

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

Lean4

theorem measurable_of_isClosed' {f : δ → γ} (hf : ∀ s, IsClosed s → s.Nonempty → s ≠ univ → MeasurableSet (f ⁻¹' s)) :
    Measurable f := by
  apply measurable_of_isClosed; intro s hs
  rcases eq_empty_or_nonempty s with h1 | h1
  · simp [h1]
  by_cases h2 : s = univ
  · simp [h2]
  exact hf s hs h1 h2

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