Commit 2025-08-21 16:04 8771400c

feat(MetricSpace/Closeds): set of nonempty compacts below a closed set is closed (#28705) This is proved in analogy with isClosed_subsets_of_isClosed. That theorem is also renamed to Closeds.isClosed_subsets_of_isClosed, to make space for NonemptyCompacts.isClosed_subsets_of_isClosed. We also rename NonemptyCompacts.ToCloseds.isUniformEmbedding to isUniformEmbedding_toCloseds to more closely match the naming convention.