Documentation

Mathlib.Topology.EMetricSpace.Paracompact

(Extended) metric spaces are paracompact #

In this file we provide two instances:

TODO #

Generalize to PseudoMetrizableSpaces.

Tags #

metric space, paracompact space, normal space

@[instance 100]

A PseudoEMetricSpace is always a paracompact space. Formalization is based on [Rud69].

Equations
  • =
theorem EMetric.t4Space {α : Type u_1} [EMetricSpace α] :