X : Type u_1
Y : Type u_2
Z : Type ?u.259336
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
X : Type u_1
Y : Type u_2
Z : Type ?u.259336
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
⊢ UniformContinuousOn f s
refine' EMetric.uniformContinuousOn_iff.2 fun ε εpos => _
X : Type u_1
Y : Type u_2
Z : Type ?u.259336
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
X : Type u_1
Y : Type u_2
Z : Type ?u.259336
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
have : Tendsto (fun d : ℝ≥0∞ => (C : ℝ≥0∞) * d ^ (r : ℝ)) (𝓝 0) (𝓝 0) :=
  ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top h0
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.259336
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : Iio δ ⊆ (fun d => ↑C * d ^ ↑r) ⁻¹' {x | (fun x => x < ε) x}
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
X : Type u_1
Y : Type u_2
Z : Type ?u.259336
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
rcases ENNReal.nhds_zero_basis.mem_iff.1 (this (gt_mem_nhds εpos)) with ⟨δ, δ0, H⟩
no goals
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.259336
inst✝² : PseudoEMetricSpace X
inst✝¹ : PseudoEMetricSpace Y
inst✝ : PseudoEMetricSpace Z
C r : ℝ≥0
f : X → Y
s t : Set X
hf : HolderOnWith C r f s
h0 : 0 < r
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun d => ↑C * d ^ ↑r) (𝓝 0) (𝓝 0)
δ : ℝ≥0∞
δ0 : 0 < δ
H : Iio δ ⊆ (fun d => ↑C * d ^ ↑r) ⁻¹' {x | (fun x => x < ε) x}
⊢ ∃ δ, δ > 0 ∧ ∀ {a : X}, a ∈ s → ∀ {b : X}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
exact ⟨δ, δ0, fun hx y hy h => (hf.edist_le hx hy).trans_lt (H h)⟩