no goals
𝕜 : Type ?u.186478
𝕜' : Type ?u.186481
E : Type u_3
E' : Type ?u.186487
F : Type ?u.186490
ι : Type u_1
𝕝 : Type u_2
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NontriviallyNormedField 𝕝
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Module 𝕝 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousSMul 𝕝 E
ε : ι → 𝕝
l : Filter ι
inst✝ : NeBot l
hε : Tendsto ε l (𝓝[{0}ᶜ] 0)
S : Set E
⊢ ∀ᶠ (n : ι) in l, ε n ≠ 0
exact hε self_mem_nhdsWithin