mathlib

5dbe8c48 - feat(topology/metric_space): a map with a contracting iterate has a fixed pt (#9760)