English
The connected component of a point x is the largest connected set containing x.
Русский
Связанная компонента точки x есть наибольшее связное множество, содержащее x.
LaTeX
$$$\\mathrm{connectedComponent}(x) = \\bigcup\\{\,s \\subseteq \\alpha \\mid \\mathrm{IsPreconnected}(s) \\land x \\in s\,\\}$$$
Lean4
/-- The connected component of a point is the maximal connected set
that contains this point. -/
def connectedComponent (x : α) : Set α :=
⋃₀ {s : Set α | IsPreconnected s ∧ x ∈ s}