residualEq_isOpen — Mathlib

English

Any Baire-measurable set differs from some open set by a meager set.

Русский

Любое множество, являющееся Бaire-измеримым, отличается от некоторого открытого множества мелким множеством.

LaTeX

$$$\\\\exists u\\\\, (\\\\mathrm{IsOpen}(u) \\\\land \\\\operatorname{Meagre}(s \\\\triangle u))$$$

Lean4

/-- Any `BaireMeasurableSet` differs from some open set by a meager set. -/
theorem residualEq_isOpen (h : BaireMeasurableSet s) : ∃ u : Set α, (IsOpen u) ∧ s =ᵇ u :=
  by
  borelize α
  rcases h with ⟨t, ht, hst⟩
  rcases ht.residualEq_isOpen with ⟨u, hu, htu⟩
  exact ⟨u, hu, hst.trans htu⟩

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