∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : PseudoMetricSpace Y] {C r : NNReal} {f : X → Y}
  {s : Set X} {x y : X}, HolderOnWith C r f s → x ∈ s → y ∈ s → dist (f x) (f y) ≤ ↑C * dist x y ^ ↑r