nLab punctured neighborhood

 Definition

In classical mathematics, let $(X, \mathcal{O}(X))$ be a topological space. A punctured neighborhood of an element $x \in X$ is the subset of a neighborhood $U$ of $x$ consisting of all elements in $U$ which are not equal to $x$, or equivalently, the relative complement $U / \{x\}$.

In constructive mathematics, let $(X, \mathcal{O}(X))$ be a topological space with a tight apartness relation $\#$. An element $x \in X$ is strictly apart from a subset $U \subseteq X$ if for all elements $y \in X$, $y \in U$ implies that $x \# y$. A punctured neighborhood of an element $x \in X$ is the subset of a neighborhood $U$ of $x$ consisting of all elements in $U$ which are strictly apart from $x$.

The tight apartness relation is needed in constructive mathematics because in the real numbers, a neighborhood around a real number $c$ is an open interval $(c - \epsilon, c + \epsilon)$ where $\epsilon$ is a positive real number, and a punctured neighborhood is the set of real numbers $x$ in the open interval $(c - \epsilon, c + \epsilon)$ where $0 \lt {|x - c|}$. The tight apartness relation $x \# c$ holds precisely if and only if $0 \lt {|x - c|}$.

 See also

• neighborhood

• limit point

• limit of a function