(Extended) metric spaces are paracompact

In this file we provide two instances:

• EMetric.instParacompactSpace: a PseudoEMetricSpace is paracompact; formalization is based on [Rud69];
• EMetric.instNormalSpace: an EMetricSpace is a normal topological space.

TODO

Generalize to PseudoMetrizableSpaces.

Tags

metric space, paracompact space, normal space

@[instance 100]

instance EMetric.instParacompactSpace {α : Type u_1} [PseudoEMetricSpace α] : ParacompactSpace α

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

Equations

• ⋯ = ⋯

theorem EMetric.t4Space {α : Type u_1} [EMetricSpace α] : T4Space α