E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) R
⊢ ∃ r, r ∈ Ioo 0 R ∧ s ⊆ ball x r
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : s ⊆ ball x R
⊢ ∃ r, r ∈ Ioo 0 R ∧ s ⊆ ball x r
rw [ball_eq_preimage, ← image_subset_iff] at h
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) R
r : ℝ
hr : r ∈ Ioo 0 R
hsr : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) r
⊢ ∃ r, r ∈ Ioo 0 R ∧ s ⊆ ball x r
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) R
⊢ ∃ r, r ∈ Ioo 0 R ∧ s ⊆ ball x r
rcases exists_pos_lt_subset_ball hR (toEuclidean.isClosed_image.2 hs) h with ⟨r, hr, hsr⟩
no goals
case intro.intro
E : Type u_1
inst✝⁶ : AddCommGroup E
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : T2Space E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
inst✝ : FiniteDimensional ℝ E
R : ℝ
s : Set E
x : E
hR : 0 < R
hs : IsClosed s
h : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) R
r : ℝ
hr : r ∈ Ioo 0 R
hsr : ↑toEuclidean '' s ⊆ Metric.ball (↑toEuclidean x) r
⊢ ∃ r, r ∈ Ioo 0 R ∧ s ⊆ ball x r
exact ⟨r, hr, image_subset_iff.1 hsr⟩