X : Type u_1
Y : Type u_2
Z : Type ?u.127575
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
b : X
⊢ edist (f b) (f b) ≤ ↑C * edist b b ^ ↑r
X : Type u_1
Y : Type u_2
Z : Type ?u.127575
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
x : X
⊢ HolderOnWith C r f {x}
rintro a (rfl : a = x) b (rfl : b = a)
X : Type u_1
Y : Type u_2
Z : Type ?u.127575
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
b : X
⊢ 0 ≤ ↑C * edist b b ^ ↑r
X : Type u_1
Y : Type u_2
Z : Type ?u.127575
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
b : X
⊢ edist (f b) (f b) ≤ ↑C * edist b b ^ ↑r
rw [edist_self]
no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.127575
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
b : X
⊢ 0 ≤ ↑C * edist b b ^ ↑r
exact zero_le _