mathlib documentation


(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:

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]