Linked points in a closure space

Statement

Two points of a closure space are linked if they are equal or their two-point set is not closed. It tests closure of a pair, without requiring an ambient topology.

Definition

Let be a set with a closure operation : the map is extensive, monotone and idempotent, with . A subset is closed when .

For , write for the relation

If , this says precisely that closing the pair adds a point outside it. The equality alternative ensures even when the singleton is closed.

The relation is symmetric, since . Reflexivity and symmetry are established by the cited elementary lemmas. Transitivity is supplied later by passing to the equivalence relation generated by linked pairs.

Assumptions

The only input is a closure space and two points . Finite-union preservation and separation properties are not assumed. The formula therefore applies even when is not a topological closure.

Conclusion

The output is the proposition that and are linked. It is the generating relation for finite-chain components: a chain may move between equal points or between points whose pair is not closed. The associated component construction is defined separately by the equivalence closure of this relation.

Main citations

• Exact relation, reflexivity and symmetry: ClosureSpace.Linked, ClosureSpace.linked_refl and ClosureSpace.linked_symm, lines 30–46.
• The meaning of closedness: ClosureSpace.closure, ClosureSpace.IsClosed and ClosureSpace.isClosed_iff, lines 37–61.
• Passing to finite-chain components: ClosureSpace.componentSetoid, ClosureSpace.Related and ClosureSpace.component, lines 49–68. This is the explanatory next construction.
• Ryotaro Tanaka, arXiv:2504.05551v1, Definition 3.20: the same generating relation and its finite-chain extension.

def Linked (c : ClosureSpace α) (x y : α) : Prop := x = y ∨ ¬ c.IsClosed {x, y}

def Linked (c : ClosureSpace α) (x y : α) : Prop := x = y ∨ ¬ c.IsClosed {x, y}

def Linked (c : ClosureSpace α) (x y : α) : Prop := x = y ∨ ¬ c.IsClosed {x, y}

def Linked (c : ClosureSpace α) (x y : α) : Prop := x = y ∨ ¬ c.IsClosed {x, y}

def Linked (c : ClosureSpace α) (x y : α) : Prop := x = y ∨ ¬ c.IsClosed {x, y}

def Linked (c : ClosureSpace α) (x y : α) : Prop := x = y ∨ ¬ c.IsClosed {x, y}