mathlib3

9061ecc1 - feat(topology/metric_space/holder): define Hölder continuity (#8309)

feat(topology/metric_space/holder): define Hölder continuity (#8309) Add definitions and some basic facts about Hölder continuous functions. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>