nLab
locally decomposable space

Locally decomposable spaces

Idea

Local decomposability is a sort of separation axiom, like a weak sort of regularity, that is trivial in classical mathematics, but interesting in constructive mathematics.

Definition

A topological space XX is locally decomposable if for any open set UXU\subseteq X and point xXx\in X, there exists an open set VV with xVx\in V such that for all yXy\in X we have either yUy\in U or yVy\notin V. If excluded middle holds, of course, we can take V=UV = U.

For point-set apartness spaces, which are equivalent to certain topological spaces, the condition can be rephrased as: if xAx\bowtie A, then there is a set BB such that xBx\bowtie B and for all yy we have either yAy\bowtie A or yBy\in B.

For uniform spaces, the notion of uniform regularity is really a notion of “uniform local decomposability”; but since in the uniform case it is sufficient to imply full regularity, we generally call it “uniform regularity” instead. For quasi-uniform spaces this is no longer true (since after all, there are non-regular quasi-uniform spaces classically), so we should speak of uniform local decomposability instead.

References

  • Douglas Bridges, Peter Schuster, and Luminita Vita, Apartness, Topology, and Uniformity: a Constructive View, doi

Last revised on January 18, 2017 at 04:23:26. See the history of this page for a list of all contributions to it.