no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.210790
𝕝 : Type ?u.210793
𝕝₂ : Type ?u.210796
E : Type u_2
F : Type ?u.210802
G : Type ?u.210805
ι : Type u_3
ι' : Type ?u.210811
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
U : Set E
⊢ IsOpen U ↔ ∀ (x : E), x ∈ U → ∃ s r, r > 0 ∧ ball (Finset.sup s p) x r ⊆ U
simp_rw [← WithSeminorms.mem_nhds_iff hp _ U, isOpen_iff_mem_nhds]