(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 Metric.instParacompactSpace {α : Type u_1} [PseudoEMetricSpace α] : ParacompactSpace α

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

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

@[deprecated Metric.t4Space (since := "2026-01-24")]

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

Alias of Metric.t4Space.