measurableSingleton_of_standardBorel

English

If α is a standard Borel space, then every singleton {a} is measurable; i.e., α has measurable singletons.

Русский

Если α — стандартное Борелево пространство, то множества-одиночки {a} измеримы.

LaTeX

$$$ \text{MeasurableSingletonClass}(α) $$$

Lean4

instance (priority := 100) measurableSingleton_of_standardBorel [StandardBorelSpace α] : MeasurableSingletonClass α :=
  letI := upgradeStandardBorel α
  inferInstance

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