toDiscreteMeasurableSpace — Mathlib

English

There is a MeasurableSingletonClass structure induced on α by the discrete measurable space when conditions hold.

Русский

Если выполнены условия, на α индуцируется класс измеримых одиночек через дискретное пространство.

LaTeX

$$$\\text{MeasurableSingletonClass }\\alpha.$$$

Lean4

instance (priority := 100) toDiscreteMeasurableSpace [MeasurableSpace α] [MeasurableSingletonClass α] [Countable α] :
    DiscreteMeasurableSpace α where forall_measurableSet _ := (Set.to_countable _).measurableSet

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