no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.128620
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C : ℝ≥0
f : X → Y
s : Set X
⊢ HolderOnWith C 1 f s ↔ LipschitzOnWith C f s
simp only [HolderOnWith, LipschitzOnWith, NNReal.coe_one, ENNReal.rpow_one]