no goals
R : Type ?u.862790
R' : Type ?u.862793
𝕜 : Type u_1
𝕜₂ : Type ?u.862799
𝕜₃ : Type ?u.862802
𝕝 : Type ?u.862805
E : Type u_2
E₂ : Type ?u.862811
E₃ : Type ?u.862814
F : Type ?u.862817
G : Type ?u.862820
ι : Type ?u.862823
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p✝ : Seminorm 𝕜 E
x y : E
r✝ : ℝ
p q : Seminorm 𝕜 E
e : E
r : ℝ
⊢ closedBall (p ⊔ q) e r = closedBall p e r ∩ closedBall q e r
simp_rw [closedBall, ← Set.setOf_and, coe_sup, Pi.sup_apply, sup_le_iff]