no goals
𝕜 : Type u_1
𝕜₂ : Type ?u.232913
𝕝 : Type ?u.232916
𝕝₂ : Type ?u.232919
E : Type u_2
F : Type u_4
G : Type ?u.232928
ι : Type u_3
ι' : Type ?u.232934
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
inst✝ : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
u : F → E
f : Filter F
y₀ : E
⊢ Filter.Tendsto u f (𝓝 y₀) ↔ ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, ↑(Finset.sup s p) (u x - y₀) < ε
simp [hp.hasBasis_ball.tendsto_right_iff]