preimage — Mathlib

English

The preimage of a Baire-measurable set under a continuous open map is Baire-measurable.

Русский

Обратное изображение множества Байе-измеримого под непрерывным открытым отображением также является Байе-измеримым.

LaTeX

$$$\\\\mathrm{BaireMeasurableSet}(f^{-1}(s))$$$

Lean4

/-- The preimage of a `BaireMeasurableSet` under a continuous open map is Baire measurable. -/
theorem preimage (hc : Continuous f) (ho : IsOpenMap f) {s : Set β} (h : BaireMeasurableSet s) :
    BaireMeasurableSet (f ⁻¹' s) := by
  rcases h with ⟨u, hu, hsu⟩
  refine ⟨f ⁻¹' u, ?_, hsu.filter_mono <| tendsto_residual_of_isOpenMap hc ho⟩
  borelize α β
  exact hc.measurable hu

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