connectedComponent — Mathlib

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}

Похожие утверждения