Version 1 source-bound exposition export. Original text SHA-256: 29d18c963b72cee77e48beb18b53b4b9e94013521bf980363adc862ba536aba9. Link targets are adapted for this edition; the registered Card identity is unchanged.

# 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 $X$ be a set with a closure operation $c:\mathcal P(X)\to\mathcal P(X)$: the map is extensive, monotone and idempotent, with $c(\varnothing)=\varnothing$. A subset $A\subseteq X$ is closed when $c(A)=A$.

For $x,y\in X$, write $x\leftrightarrow_c y$ for the relation

$$
x\leftrightarrow_c y
\quad\Longleftrightarrow\quad
x=y\ \text{ or }\ c(\{x,y\})\ne\{x,y\}.
$$

If $x\ne y$, this says precisely that closing the pair adds a point outside it. The equality alternative ensures $x\leftrightarrow_c x$ even when the singleton $\{x\}$ is closed.

The relation is symmetric, since $\{x,y\}=\{y,x\}$. 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 $(X,c)$ and two points $x,y\in X$. Finite-union preservation and separation properties are not assumed. The formula therefore applies even when $c$ is not a topological closure.

## Conclusion

The output is the proposition that $x$ and $y$ 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](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/Components.lean.html?from=7&start=30&end=46&ranges=30-46#L30): `ClosureSpace.Linked`, `ClosureSpace.linked_refl` and `ClosureSpace.linked_symm`, lines 30–46.
- [The meaning of closedness](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/Basic.lean.html?from=7&start=37&end=61&ranges=37-61#L37): `ClosureSpace.closure`, `ClosureSpace.IsClosed` and `ClosureSpace.isClosed_iff`, lines 37–61.
- [Passing to finite-chain components](https://exactmathematics.org/mathlibannex/sources/gss-v0.5.0/MathlibAnnex/Topology/ClosureSpace/Components.lean.html?from=7&start=49&end=68&ranges=49-68#L49): `ClosureSpace.componentSetoid`, `ClosureSpace.Related` and `ClosureSpace.component`, lines 49–68. This is the explanatory next construction.
- Ryotaro Tanaka, [arXiv:2504.05551v1, Definition 3.20](https://arxiv.org/pdf/2504.05551v1#page=10): the same generating relation and its finite-chain extension.

## Lean source signature (exact)

The namespace is `ClosureSpace`; the surrounding carrier `α` denotes the set $X$.

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

| In the source | Mathematical meaning |
| --- | --- |
| `α`, `c : ClosureSpace α` | The underlying set $X$ and the closure structure $c$: an extensive, monotone, idempotent operation on $\mathcal P(X)$ that preserves $\varnothing$. The operation itself is `c.closure`. |
| `x y : α` | The two given points $x,y\in X$; no distinctness is required. |
| `c.IsClosed {x, y}` | The equality $c(\{x,y\})=\{x,y\}$. |
| `x = y ∨ ¬ c.IsClosed {x, y}` | The entire defining proposition $x=y$ or $c(\{x,y\})\ne\{x,y\}$. The disjunction retains the equality case, and the negation applies to closedness of the pair. |
| `: Prop` | The output is the linked-pair relation $x\leftrightarrow_c y$, before taking any transitive closure or component. |