English
A map f: X → Y is separated if whenever f(x1)=f(x2) with x1 ≠ x2, there exist disjoint open neighborhoods separating x1 and x2.
Русский
Функция f: X→Y разделена, если при равенстве значений и различии точек можно найти попарно непересекающиеся открытые окрестности.
LaTeX
$$$$\\operatorname{IsSeparatedMap}(f) \\iff \\forall x_1,x_2, f(x_1)=f(x_2) \\to x_1 \\neq x_2 \\to \\exists s_1,s_2,\\ \\mathrm{IsOpen}(s_1) \\land \\mathrm{IsOpen}(s_2) \\land x_1\\in s_1 \\land x_2\\in s_2 \\land \\operatorname{Disjoint}(s_1,s_2).$$$$
Lean4
/-- A function from a topological space `X` to a type `Y` is a separated map if any two distinct
points in `X` with the same image in `Y` can be separated by open neighborhoods. -/
def IsSeparatedMap (f : X → Y) : Prop :=
∀ x₁ x₂, f x₁ = f x₂ → x₁ ≠ x₂ → ∃ s₁ s₂, IsOpen s₁ ∧ IsOpen s₂ ∧ x₁ ∈ s₁ ∧ x₂ ∈ s₂ ∧ Disjoint s₁ s₂
