Commit 2025-02-10 18:44 f64765bd

chore(Topology/MetricSpace/Pseudo): move lemmas downstream (#21644) I am looking at the import graph of Topology/MetricSpace/Defs.lean and noticing two clusters of gray imports: one via UniformSpace/Compact.lean and another via Data/ENNReal/Inv.lean. This PR attempts to address the first. In MetricSpace/Pseudo/Defs.lean we import UniformSpace/Compact.lean to prove finite_cover_balls_of_compact and lebesgue_number_lemma_of_metric. It seems these are only usedin files that already import Pseudo/Lemmas.lean, so we can move them downstream to shake that import.

• finite_cover_balls_of_compact only needs imports that are already available in Pseudo/Basic.lean, so we can move it there.
• lebesgue_number_lemma_of_metric really needs UniformSpace/Compact.lean, so we move it to Pseudo/Lemmas.lean and readd the import of UniformSpace/Compact.lean.