case intro
X : Type u_1
Y : Type u_2
Z : Type ?u.969277
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : dist x y ≤ ↑d
⊢ dist (f x) (f y) ≤ ↑C * ↑d ^ ↑r
X : Type u_1
Y : Type u_2
Z : Type ?u.969277
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ
hd : dist x y ≤ d
⊢ dist (f x) (f y) ≤ ↑C * d ^ ↑r
lift d to ℝ≥0 using dist_nonneg.trans hd
case intro
X : Type u_1
Y : Type u_2
Z : Type ?u.969277
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
case intro
X : Type u_1
Y : Type u_2
Z : Type ?u.969277
inst✝¹ : PseudoMetricSpace X
inst✝ : PseudoMetricSpace Y
C r : ℝ≥0
f : X → Y
hf : HolderWith C r f
x y : X
d : ℝ≥0
hd : dist x y ≤ ↑d
⊢ dist (f x) (f y) ≤ ↑C * ↑d ^ ↑r
rw [dist_nndist] at hd⊢
case intro
X : Type u_1
Y : Type u_2
Z : Type ?u.969277
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
case intro
X : Type u_1
Y : Type u_2
Z : Type ?u.969277
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  at hd⊢
no goals
case intro
X : Type u_1
Y : Type u_2
Z : Type ?u.969277
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
exact hf.nndist_le_of_le hd