English
Let α be a topological space and s a Borel subset of α. There exists an open set u such that s and u differ by a meager set; i.e., s equals an open set up to a meager remainder.
Русский
Пусть α — топологическое пространство, и s — борелевское множество в α. Существует открытое множество u, такое что s и u отличаются мелким множеством, то есть s совпадает с открытым множеством за пределами мелкого множества.
LaTeX
$$$\\\\exists u\\\\, (\\\\mathrm{IsOpen}(u) \\\\land \\\\operatorname{Meagre}(s \\\\triangle u))$$$
Lean4
/-- Any Borel set differs from some open set by a meager set. -/
theorem residualEq_isOpen [MeasurableSpace α] [BorelSpace α] (h : MeasurableSet s) : ∃ u : Set α, IsOpen u ∧ s =ᵇ u :=
by
induction s, h using MeasurableSet.induction_on_open with
| isOpen U hU => exact ⟨U, hU, .rfl⟩
| compl s _ ihs =>
obtain ⟨U, Uo, hsU⟩ := ihs
use (closure U)ᶜ, isClosed_closure.isOpen_compl
exact .compl <| hsU.trans <| .symm <| closure_residualEq Uo.isLocallyClosed
| iUnion f _ _ ihf =>
choose u uo su using ihf
exact ⟨⋃ i, u i, isOpen_iUnion uo, EventuallyEq.countable_iUnion su⟩
