import Mathlib.Topology.MetricSpace.Pseudo.Lemmas

#check lebesgue_number_lemma_of_metric