English
Let f: X → Y be a map between topological spaces. Then f is a separated map if and only if for all x1, x2 in X with f(x1) = f(x2) and x1 ≠ x2 there exist neighborhoods s1 of x1 and s2 of x2 such that s1 and s2 are disjoint.
Русский
Пусть f: X → Y — отображение между топологическими пространствами. Тогда f есть разделяющее отображение тогда и только тогда, для любых x1, x2 ∈ X с f(x1) = f(x2) и x1 ≠ x2 существуют окрестности s1 вокруг x1 и s2 вокруг x2, такие что s1 ∩ s2 = ∅.
LaTeX
$$$\mathrm{IsSeparatedMap}(f) \iff \forall x_1,x_2, \; f(x_1)=f(x_2) \to x_1 \neq x_2 \to \exists s_1 \in \nhds(x_1), \exists s_2 \in \nhds(x_2), \operatorname{Disjoint}(s_1,s_2)$$$
Lean4
theorem isSeparatedMap_iff_nhds {f : X → Y} :
IsSeparatedMap f ↔ ∀ x₁ x₂, f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ ∈ 𝓝 x₁, ∃ s₂ ∈ 𝓝 x₂, Disjoint s₁ s₂ := by
simp_rw [isSeparatedMap_iff_disjoint_nhds, Filter.disjoint_iff]
