case inl
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f (closedBall x 0)

case inr
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closedBall x r)
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
⊢ ContinuousOn f (closedBall x r)
rcases eq_or_ne r 0 with (rfl | hr)
case inl
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f {x}
case inl
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f (closedBall x 0)
rw [closedBall_zero]
no goals
case inl
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
h : DiffContOnCl 𝕜 f (ball x 0)
⊢ ContinuousOn f {x}
exact continuousOn_singleton f x
case inr
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure (ball x r))
case inr
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closedBall x r)
rw [← closure_ball x hr]
no goals
case inr
𝕜 : Type u_2
E : Type u_1
F : Type u_3
G : Type ?u.8350
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedSpace 𝕜 F
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f g : E → F
s t : Set E
x✝ : E
inst✝ : NormedSpace ℝ E
x : E
r : ℝ
h : DiffContOnCl 𝕜 f (ball x r)
hr : r ≠ 0
⊢ ContinuousOn f (closure (ball x r))
exact h.continuousOn