no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.128203
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
⊢ HolderOnWith C r f univ ↔ HolderWith C r f
simp only [HolderOnWith, HolderWith, mem_univ, true_imp_iff]