rw [(nhdsWithin_hasBasis nhds_basis_closedBall (Ioi (0 : ℝ))).eventually_iff]
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∀ᶠ (t : ℝ) in 𝓝[>] 0, φ t ⊆ s
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∃ i, 0 < i ∧ ∀ ⦃x : ℝ⦄, x ∈ closedBall 0 i ∩ Ioi 0 → φ x ⊆ s