case intro.intro
𝕜 : Type ?u.302548
E : Type u_1
F : Type ?u.302554
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r✝ : ℝ
x : E
hc : Convex ℝ s
h₀ : s ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : Metric.ball 0 r ⊆ s
⊢ UniformContinuous (gauge s)
𝕜 : Type ?u.302548
E : Type u_1
F : Type ?u.302554
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r : ℝ
x : E
hc : Convex ℝ s
h₀ : s ∈ 𝓝 0
⊢ UniformContinuous (gauge s)
obtain ⟨r, hr₀, hr⟩ := Metric.mem_nhds_iff.1 h₀
case intro.intro.intro
𝕜 : Type ?u.302548
E : Type u_1
F : Type ?u.302554
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r✝ : ℝ
x : E
hc : Convex ℝ s
h₀ : s ∈ 𝓝 0
r : ℝ≥0
hr₀ : ↑r > 0
hr : Metric.ball 0 ↑r ⊆ s
⊢ UniformContinuous (gauge s)
case intro.intro
𝕜 : Type ?u.302548
E : Type u_1
F : Type ?u.302554
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r✝ : ℝ
x : E
hc : Convex ℝ s
h₀ : s ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : Metric.ball 0 r ⊆ s
⊢ UniformContinuous (gauge s)
lift r to ℝ≥0 using le_of_lt hr₀
no goals
case intro.intro.intro
𝕜 : Type ?u.302548
E : Type u_1
F : Type ?u.302554
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
r✝ : ℝ
x : E
hc : Convex ℝ s
h₀ : s ∈ 𝓝 0
r : ℝ≥0
hr₀ : ↑r > 0
hr : Metric.ball 0 ↑r ⊆ s
⊢ UniformContinuous (gauge s)
exact (hc.lipschitzWith_gauge hr₀ hr).uniformContinuous