measurableAtom_of_measurableSingletonClass

English

If the space has a measurable singleton structure, then each atom is exactly the singleton {x}.

Русский

Если пространство имеет свойство измеримой одинарности, то атом равен множеству {x}.

LaTeX

$$$$ \operatorname{measurableAtom}(x) = \{x\} $$$$

Lean4

@[simp]
theorem measurableAtom_of_measurableSingletonClass [MeasurableSingletonClass β] (x : β) : measurableAtom x = { x } :=
  Subset.antisymm (measurableAtom_subset (measurableSet_singleton x) rfl) (by simp)

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