mathlib

a1bdaddf - chore(topology/metric_space/hausdorff_distance): move two lemmas (#12771)

chore(topology/metric_space/hausdorff_distance): move two lemmas (#12771) Remove the dependence of `topology/metric_space/hausdorff_distance` on `analysis.normed_space.basic`, by moving out two lemmas.