mathlib3

5316314b - feat(topology/metric_space/infsep): Add "infimum separation". (#15689)

feat(topology/metric_space/infsep): Add "infimum separation". (#15689) Informally, this is the "minimum distance", though "minimum" makes sense mainly only in the finite context. This is analogous to diam in some sense. We provide finset and set versions for both the emetric and metric cases. We generally try to have the analogous lemmas that diam has, and any other useful utility lemmas to allow for the use of the definition without unpacking it.