mathlib

e623a7e4 - fix(topology/metric_space/lipschitz): typo (#16962)