X : Type u_1
Y : Type u_2
Z : Type ?u.903365
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r
X : Type u_1
Y : Type u_2
Z : Type ?u.903365
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ ↑(nndist (f x) (f y)) ≤ ↑C * ↑d ^ ↑r
norm_cast
X : Type u_1
Y : Type u_2
Z : Type ?u.903365
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist (f x) (f y) ≤ ↑C * ↑d ^ ↑r
X : Type u_1
Y : Type u_2
Z : Type ?u.903365
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ nndist (f x) (f y) ≤ C * d ^ ↑r
rw [← ENNReal.coe_le_coe, ← edist_nndist, ENNReal.coe_mul, ←
  ENNReal.coe_rpow_of_nonneg _ r.coe_nonneg]
X : Type u_1
Y : Type u_2
Z : Type ?u.903365
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist x y ≤ ↑d
X : Type u_1
Y : Type u_2
Z : Type ?u.903365
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist (f x) (f y) ≤ ↑C * ↑d ^ ↑r
apply hf.edist_le_of_le
no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.903365
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : nndist x y ≤ d
⊢ edist x y ≤ ↑d
rwa [edist_nndist, ENNReal.coe_le_coe]