mathlib documentation

topology.metric_space.emetric_paracompact

(Extended) metric spaces are paracompact #

In this file we provide two instances:

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 α] :