no goals
α : Type u_1
β : Type ?u.19471
σ : Type ?u.19474
τ : Type ?u.19477
inst✝ : TopologicalSpace α
F : Realizer α
s : F.σ
a : α
m : a ∈ f F.F s
⊢ 𝓝 a ≤ 𝓟 (f F.F s)
simpa using F.mem_nhds.2 ⟨s, m, Subset.refl _⟩