Neighbourhood

Set

 context $\langle X,\mathcal{T}_X\rangle$ … topological space context $p\in X$ definiendum $U_p\in\mathrm{it}$ postulate $\exists(\mathcal{O}\in\mathcal{T}_X).\ \mathcal{O}\subseteq U_p$

Discussion

A neighbourhood of $p$ is a reasonably big set surrounding $p$.

Predicates

Consider $X$ together with a topology, then

locally euclidean space means $X$ is homeomorphic to $\mathbb R^n$:

 predicate $X$ … locally euclidean space $\equiv \forall(x\in X).\ \exists(U_x\in\mathrm{Neighbourhood}(x)),\ f.\ f\in\mathrm{Homeomorphism}(U_x,\mathbb R^n)$

topoloical manifold means Hausdorff space + locally euclidean space:

 predicate $X$ … topoloical manifold $\equiv X$ … Hausdorff space, locally euclidean space