separatesPoints_of_measurableSingletonClass

English

If a space has a measurable singleton class and is countable, it separates points.

Русский

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

LaTeX

$$$ [MeasurableSpace \\alpha] [Countable \\alpha] [SeparatesPoints \\alpha] : SeparatesPoints \\alpha $$$

Lean4

instance (priority := 100) separatesPoints_of_measurableSingletonClass [MeasurableSpace α]
    [MeasurableSingletonClass α] : SeparatesPoints α :=
  by
  refine ⟨fun x y h ↦ ?_⟩
  specialize h _ (MeasurableSet.singleton x)
  simp_rw [mem_singleton_iff, forall_true_left] at h
  exact h.symm

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