Components generated by linked pairs

Statement

The component of a point in a closure space consists of all points reachable from it by a finite chain of linked pairs. It is represented as an actual subset of the original set.

Definition

Let be a set with an extensive, monotone and idempotent closure operation satisfying . A subset is closed when . Define

Let mean that there is an integer and a finite chain

The case is the chain with a single point, so it gives . The component of is

The source defines as the equivalence relation generated by the linked relation. This agrees with the finite-chain description: the linked relation is symmetric, reversing a chain gives symmetry, and concatenating two chains gives transitivity. The empty chain of steps supplies reflexivity. These are exactly the operations in the cited equivalence-closure construction.

Assumptions

The only data are a closure space and a point . No topology or separation condition is required. If is empty, there is no point at which to evaluate the component function.

Conclusion

The result is the subset , which contains . The separately cited equality criterion gives

Thus choosing another point in the same component leaves the component set unchanged. Its closure is a separate object, defined separately in the source. The definition of does not assert that this subset is closed or that it is a connected component in a topological sense.

Main citations

• The generating relation and equivalence closure: ClosureSpace.Linked, ClosureSpace.componentSetoid and ClosureSpace.Related, lines 30–65.
• Exact component, membership and the separate component closure: ClosureSpace.component, ClosureSpace.mem_component, ClosureSpace.component_eq_of_related and ClosureSpace.componentClosure, lines 68–84.
• Equality of component sets: ClosureSpace.component_eq_iff_related, lines 30–37.
• The finite equivalence-closure constructors: Mathlib Relation.EqvGen, lines 349–353, at the pinned mathlib commit. Its constructors insert relation steps, reflexivity, symmetry and transitivity.
• Ryotaro Tanaka, arXiv:2504.05551v1, Definition 3.20, Proposition 3.23 and Definition 3.24: the finite-chain relation; the component notation continues on page 11.

def component (c : ClosureSpace α) (x : α) : Set α := {y | c.Related x y}

def component (c : ClosureSpace α) (x : α) : Set α := {y | c.Related x y}

def component (c : ClosureSpace α) (x : α) : Set α := {y | c.Related x y}

def component (c : ClosureSpace α) (x : α) : Set α := {y | c.Related x y}

def component (c : ClosureSpace α) (x : α) : Set α := {y | c.Related x y}

def component (c : ClosureSpace α) (x : α) : Set α := {y | c.Related x y}

variable (r) in
/-- `EqvGen r`: equivalence closure of `r`. -/
@[mk_iff]
inductive EqvGen : α → α → Prop
  | rel x y : r x y → EqvGen x y
  | refl x : EqvGen x x
  | symm x y : EqvGen x y → EqvGen y x
  | trans x y z : EqvGen x y → EqvGen y z → EqvGen x z