baireMeasurableSet — Mathlib

English

If s is a measurable set (with respect to a Borel structure), then s is BaireMeasurableSet.

Русский

Если множество является измеримым в бореллевом смысле, то оно Баирово измеримо.

LaTeX

$$$$ \text{MeasurableSet}(s) \Rightarrow \mathrm{BaireMeasurableSet}(s). $$$$

Lean4

theorem _root_.MeasurableSet.baireMeasurableSet [MeasurableSpace α] [BorelSpace α] (h : MeasurableSet s) :
    BaireMeasurableSet s := by
  borelize α
  exact h.eventuallyMeasurableSet

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