iff_residualEq_isOpen — Mathlib

English

A set is Baire-measurable if and only if it differs from some open set by a meager set.

Русский

Множество является Бaire-измеримым тогда и только тогда, когда оно отличается от некоторого открытого множества мелким множеством.

LaTeX

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

Lean4

/-- A set is Baire measurable if and only if it differs from some open set by a meager set. -/
theorem iff_residualEq_isOpen : BaireMeasurableSet s ↔ ∃ u : Set α, (IsOpen u) ∧ s =ᵇ u :=
  ⟨fun h => h.residualEq_isOpen, fun ⟨_, uo, ueq⟩ => uo.baireMeasurableSet.congr ueq.symm⟩

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