no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.207750
𝕝 : Type ?u.207753
𝕝₂ : Type ?u.207756
E : Type u_2
F : Type ?u.207762
G : Type ?u.207765
ι : Type u_3
ι' : Type ?u.207771
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
x : E
U : Set E
⊢ U ∈ 𝓝 x ↔ ∃ s r, r > 0 ∧ ball (Finset.sup s p) x r ⊆ U
rw [hp.hasBasis_ball.mem_iff, Prod.exists]