Metric.isClosed_ball later than Defs file

Stream: mathlib4

[Yakov Pechersky]

docs#Metric.isClosed_ball (and also about a sphere) is proven using a more conceptual proof, but in Mathlib.Topology.MetricSpace.Pseudo.Lemmas, not in Mathlib.Topology.MetricSpace.Pseudo.Defs. Is that desired, or would it make sense to use a more primitive proof in Defs?

[Yury G. Kudryashov]

Do we have reasons to have this lemma available earlier in the import graph?

[Yury G. Kudryashov]

IMHO, Defs files are for definitions and basic theorems unfolding these definitions.

[Yakov Pechersky]

The openness of a open ball is in Defs, and I thought we try to prove what we can at the site-of-declaration. Not a big issue to import Lemmas over Defs. Lemmas ends up pulling in more files about Order.IsLUB, DenselyOrdered, some bornology constructions, and things about intervals.

[Yaël Dillies]

I was the one splitting the file this way and many lemmas ended up in Lemmas solely because they depend on isClosed_ball

[Yury G. Kudryashov]

If we're worried about imports, then we can split Lemmas into smaller files (and move more from Defs - as I wrote above, I think that these files are for definitions only).

[Yury G. Kudryashov]

I don't think that we should use more complicated proofs for no reason.

[Yury G. Kudryashov]

E.g., I don't think that docs#Metric.totallyBounded_of_finite_discretization belongs in a Defs file.