English
The measurable atom of a point x in β is defined as the intersection of all measurable sets containing x; it is measurable when the space is countably generated.
Русский
Измеримая атома точки x в β определяется как пересечение всех измеримых множеств, содержащих x; она измерима, когда пространство счетно порождено.
LaTeX
$$$\\text{measurableAtom}(x) \= \\bigcap_{s \\subseteq \\beta,\, x \\in s,\, \\text{MeasurableSet}(s)} s$$$
Lean4
/-- The *measurable atom* of `x` is the intersection of all the measurable sets containing `x`.
It is measurable when the space is countable (or more generally when the measurable space is
countably generated). -/
def measurableAtom (x : β) : Set β :=
⋂ (s : Set β) (_h's : x ∈ s) (_hs : MeasurableSet s), s
