instMeasurableSingletonClass — Mathlib

English

If the ambient space has a measurable singleton class, then the NullMeasurableSpace has a measurable singleton class.

Русский

Если вокруг имеется класс измеримых одиничных множеств, то NullMeasurableSpace имеет такой же класс.

LaTeX

$$$[\\text{MeasurableSingletonClass } \\alpha] \\Rightarrow [\\text{MeasurableSingletonClass (NullMeasurableSpace } \\alpha \\mu)]$$$

Lean4

instance instMeasurableSingletonClass [MeasurableSingletonClass α] :
    MeasurableSingletonClass (NullMeasurableSpace α μ) :=
  eventuallyMeasurableSingleton (m := m0)

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