English
For a measurable space α, the property SeparatesPoints α is equivalent to the following: for all x,y in α, if for every measurable set s we have x ∈ s ↔ y ∈ s, then x = y.
Русский
Для измеримого пространства α свойство SeparatesPoints α эквивалентно следующему: для любых x,y в α, если для любого измеримого множества s выполняется x ∈ s ↔ y ∈ s, то x = y.
LaTeX
$$$ [MeasurableSpace \\alpha] : SeparatesPoints \\alpha \\iff \\forall x,y: \\alpha, (\\forall s, MeasurableSet s \\rightarrow (x \\in s \\leftrightarrow y \\in s)) \\rightarrow x = y $$$
Lean4
theorem separatesPoints_iff [MeasurableSpace α] :
SeparatesPoints α ↔ ∀ x y : α, (∀ s, MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y :=
⟨fun h ↦ fun _ _ hxy ↦ h.separates _ _ fun _ hs xs ↦ (hxy _ hs).mp xs, fun h ↦
⟨fun _ _ hxy ↦ h _ _ fun _ hs ↦ ⟨fun xs ↦ hxy _ hs xs, not_imp_not.mp fun xs ↦ hxy _ hs.compl xs⟩⟩⟩
