see also algebraic topology, functional analysis and homotopy theory
topological space (see also locale)
fiber space, space attachment
Kolmogorov space, Hausdorff space, regular space, normal space
sequentially compact, countably compact, locally compact, sigma-compact, paracompact, countably paracompact, strongly compact
subsets are closed in a closed subspace precisely if they are closed in the ambient space
closed subspaces of compact Hausdorff spaces are equivalently compact subspaces
open subspaces of compact Hausdorff spaces are locally compact
compact spaces equivalently have converging subnet of every net
paracompact Hausdorff spaces equivalently admit subordinate partitions of unity
injective proper maps to locally compact spaces are equivalently the closed embeddings
locally compact and second-countable spaces are sigma-compact
Theorems
Point-free topology (often referred to as pointless topology Johnstone 83 ) is any formulation of topology not based on the notion of topological space as a set of points equipped with extra structure. (A pointless space must still be this set with extra stuff, of course, as long as there is a functor mapping a space to its set of points.) Pointless topology has points, but they are not fundamental; and a particular space may well have no points and yet be far from empty.
In locale theory, for example, one studies the set of open subspaces (with the extra structure of a frame) as the fundamental notion. In formal topology, one studies a set of basic open subspaces (with the extra structure of a posite with positivity, although the isomorphisms of formal spaces don't respect these sets).
In contrast, the traditional way of doing topology using points may be called pointwise topology.
In the interest of considering whether a formulation of topology is pointless or not, I offer the following sociomathematical suggestion at a definition:
Working in a given logical context $\mathcal{L}$, suppose that one defines a category (or $(\infty,1)$-category) $S$, whose objects one thinks of as spaces and whose morphisms one thinks of as continuous maps. Suppose further that one intends $Hom(X,Y)$ to be the set (or $\infty$-groupoid) of all continuous maps from $X$ to $Y$ (whereas $Ob(S)$ need not be the class of all spaces). Also suppose that $S$ has a terminal object $pt$, which one interprets as the point.
The above is a pointwise formulation of topology if it is provable (in $\mathcal{L}$) that $pt$ is a generator in $S$ but pointless if this is not provable. (One could have stronger notions of pointlessness by asking that this be refutable; if using intuitionistic logic, this could be further strengthened.)
An introduction to locale theory is
This is, in its own words, to be read as the trailer for Johnstone’s book Stone Spaces, which see.
For formal topology, see
Giovanni Sambin (2001); Some points in formal topology; pdf.
Erik Palmgren, From Intuitionistic to Point-Free Topology: On the Foundation of Homotopy Theory, Logicism, Intuitionism, and Formalism Volume 341 of the series Synthese Library pp 237-253, 2005 (pdf)