eventuallyMeasurableSingleton — Mathlib

English

Every singleton set is EventuallyMeasurable under an appropriate MeasurableSingletonClass.

Русский

Каждое множесто-одиночка измеримо в пространстве eventuallyMeasurableSpace, если есть подходящий MeasurableSingletonClass.

LaTeX

$$$\text{eventuallyMeasurableSingleton} \;:\; \text{MeasurableSingletonClass }\alpha.$$$

Lean4

instance eventuallyMeasurableSingleton [MeasurableSingletonClass α] :
    @MeasurableSingletonClass α (eventuallyMeasurableSpace m l) :=
  @MeasurableSingletonClass.mk _ (_) <| fun x => (MeasurableSet.singleton x).eventuallyMeasurableSet

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