20.3. Properties of Topological Spaces🔗

Some properties have both a form for sets as well as the whole space. For example, IsCompact is a predicate on Set X while CompactSpace states that X itself is compact. Note that CompactSpace is a typeclass while IsCompact is not.

Some other common properties that follow this are:

• IsConnected and ConnectedSpace;

• IsPathConnected and PathConnectedSpace;

Unlike some textbook conventions, IsConnected includes nonemptiness. Use IsPreconnected when the empty set should count.

Some common separation properties are:

• Hausdorff and locally compact: T2Space and LocallyCompactSpace;

• first/second countable: FirstCountableTopology and SecondCountableTopology;

• separable and discrete: TopologicalSpace.SeparableSpace and DiscreteTopology.

As an example using some of these properties, lets look at the proof that a continuous function from a compact space to a Hausdorff space is closed.