case inl
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x (sᶜ) = 0
⊢ closedBall x (infDist x (sᶜ)) ⊆ closure s

case inr
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x (sᶜ) ≠ 0
⊢ closedBall x (infDist x (sᶜ)) ⊆ closure s
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
⊢ closedBall x (infDist x (sᶜ)) ⊆ closure s
cases' eq_or_ne (infDist x (sᶜ)) 0 with h₀ h₀
case inl
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x (sᶜ) = 0
⊢ closure {x} ⊆ closure s
case inl
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x (sᶜ) = 0
⊢ closedBall x (infDist x (sᶜ)) ⊆ closure s
rw [h₀, closedBall_zero']
no goals
case inl
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x (sᶜ) = 0
⊢ closure {x} ⊆ closure s
exact closure_mono (singleton_subset_iff.2 hx)
case inr
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x (sᶜ) ≠ 0
⊢ closure (ball x (infDist x (sᶜ))) ⊆ closure s
case inr
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x (sᶜ) ≠ 0
⊢ closedBall x (infDist x (sᶜ)) ⊆ closure s
rw [← closure_ball x h₀]
no goals
case inr
𝕜 : Type ?u.62428
inst✝⁴ : NormedField 𝕜
E : Type ?u.62434
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_1
inst✝¹ : SeminormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
s : Set F
hx : x ∈ s
h₀ : infDist x (sᶜ) ≠ 0
⊢ closure (ball x (infDist x (sᶜ))) ⊆ closure s
exact closure_mono ball_infDist_compl_subset