no goals
𝕜 : Type u_2
𝕜₂ : Type ?u.8369
𝕝 : Type ?u.8372
𝕝₂ : Type ?u.8375
E : Type u_1
F : Type ?u.8381
G : Type ?u.8384
ι : Type u_3
ι' : Type ?u.8390
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
⊢ U ∈ basisSets p ↔ ∃ i r x, U = ball (Finset.sup i p) 0 r
simp only [basisSets, mem_iUnion, mem_singleton_iff]