mathlib

626489ad - feat(topology/metric_space): diameter of a set in metric spaces (#651)