def HolderContinuity.IsHolderContinuous {X : Type u_1} {Y : Type u_2} [PseudoEMetricSpace X] [PseudoEMetricSpace Y] (α : NNReal) (f : X → Y) : Prop

Definition 9.6.5 (Hölder continuity). A function $f : X \to Y$ between pseudo-emetric spaces is $\alpha$-Hölder continuous if there exists a constant $C \ge 0$ such that $d(f(x), f(y)) \le C \cdot d(x, y)^{\alpha}$ for all $x, y \in X$.