measurableSingletonClass — Mathlib

English

If the underlying type is a subsingleton, it carries a MeasurableSingletonClass.

Русский

Если тип является подсинглтонами, то на нём есть класс измеримых синглтонов.

LaTeX

$$$[Subsingleton\;\alpha] \Rightarrow \text{MeasurableSingletonClass } \alpha.$$$

Lean4

instance (priority := 100) measurableSingletonClass {α} [MeasurableSpace α] [Subsingleton α] :
    MeasurableSingletonClass α := by
  refine ⟨fun i => ?_⟩
  convert MeasurableSet.univ
  simp [Set.eq_univ_iff_forall, eq_iff_true_of_subsingleton]

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