R : Type ?u.1320429
R' : Type ?u.1320432
𝕜 : Type u_2
𝕜₂ : Type ?u.1320438
𝕜₃ : Type ?u.1320441
𝕝 : Type ?u.1320444
E : Type u_1
E₂ : Type ?u.1320450
E₃ : Type ?u.1320453
F : Type ?u.1320456
G : Type ?u.1320459
ι : Type ?u.1320462
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (⋂ (ρ : ℝ) (_ : ρ > r), ball p x ρ)
R : Type ?u.1320429
R' : Type ?u.1320432
𝕜 : Type u_2
𝕜₂ : Type ?u.1320438
𝕜₃ : Type ?u.1320441
𝕝 : Type ?u.1320444
E : Type u_1
E₂ : Type ?u.1320450
E₃ : Type ?u.1320453
F : Type ?u.1320456
G : Type ?u.1320459
ι : Type ?u.1320462
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (closedBall p x r)
rw [closedBall_eq_biInter_ball]
no goals
R : Type ?u.1320429
R' : Type ?u.1320432
𝕜 : Type u_2
𝕜₂ : Type ?u.1320438
𝕜₃ : Type ?u.1320441
𝕝 : Type ?u.1320444
E : Type u_1
E₂ : Type ?u.1320450
E₃ : Type ?u.1320453
F : Type ?u.1320456
G : Type ?u.1320459
ι : Type ?u.1320462
inst✝⁵ : NormedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : NormedSpace ℝ 𝕜
inst✝² : Module 𝕜 E
inst✝¹ : Module ℝ E
inst✝ : IsScalarTower ℝ 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ Convex ℝ (⋂ (ρ : ℝ) (_ : ρ > r), ball p x ρ)
exact convex_iInter₂ fun _ _ => convex_ball _ _ _