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