separatesPointsOfOpensMeasurableSpaceOfT0Space

English

For a T0 space α with OpensMeasurableSpace structure, measurable space separates points.

Русский

Для T0-пространства α с структурой OpensMeasurableSpace сигма-алгебра разделяет точки.

LaTeX

$$$\\text{OpensMeasurableSpace.separatesPoints }\\alpha$.$$

Lean4

instance separatesPointsOfOpensMeasurableSpaceOfT0Space [T0Space α] : MeasurableSpace.SeparatesPoints α where
  separates x
    y := by
    contrapose!
    exact fun a => exists_measurableSet_of_ne a

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