English
Define a relation on α by x ∼ y iff connectedComponent(x) = connectedComponent(y). This relation is an equivalence relation; its equivalence classes are exactly the connected components of α.
Русский
Определим на основе множества α отношение x ∼ y, если connectedComponent(x) = connectedComponent(y). Это отношение эквивалентности; классы эквивалентности совпадают со связными компонентами пространства.
LaTeX
$$$x \sim y \iff \operatorname{connectedComponent}(x) = \operatorname{connectedComponent}(y)$$$
Lean4
/-- The setoid of connected components of a topological space -/
def connectedComponentSetoid (α : Type*) [TopologicalSpace α] : Setoid α :=
⟨fun x y => connectedComponent x = connectedComponent y,
⟨fun x => by trivial, fun h1 => h1.symm, fun h1 h2 => h1.trans h2⟩⟩
