(Extended) metric spaces are paracompact #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we provide two instances:

emetric.paracompact_space: a pseudo_emetric_space is paracompact; formalization is based on [Rud69];
emetric.normal_of_metric: an emetric_space is a normal topological space.

Tags #

metric space, paracompact space, normal space

@[protected, instance]

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

@[protected, instance]

def emetric.normal_of_emetric {α : Type u_1} [emetric_space α] :