English
A Baire Measurable Set is a set that differs from some Borel set by a meager set; this collection forms a σ-algebra.
Русский
Множество называется Баировым измеримым, если оно отличается от некоторого бореллевого множества с помощью множества, обладающего малостью; такая σ-алгебра закрыта.
LaTeX
$$$$ \text{BaireMeasurableSet}(s) \;\text{iff}\; \exists B \in \text{Borel}(\alpha) : s \triangle B \text{ is meager}. $$$$
Lean4
/-- We say a set is a `BaireMeasurableSet` if it differs from some Borel set by
a meager set. This forms a σ-algebra.
It is equivalent, and a more standard definition, to say that the set differs from
some *open* set by a meager set. See `BaireMeasurableSet.iff_residualEq_isOpen` -/
def BaireMeasurableSet (s : Set α) : Prop :=
@MeasurableSet _ (eventuallyMeasurableSpace (borel _) (residual _)) s
