eventually nhds

Stream: Is there code for X?

[Winston Yin (尹維晨)]

Do we have or want this?

import Mathlib.Topology.Basic
import Mathlib.Topology.Defs.Filter

example {α : Type*} [TopologicalSpace α] (p : α → Prop) (x₀ : α)
    (h : ∀ᶠ x in nhds x₀, p x) : p x₀ :=
  have ⟨_, hs, h⟩ := Filter.eventually_iff_exists_mem.mp h
  h x₀ (mem_of_mem_nhds hs)

[Etienne Marion]

@loogle Filter.Eventually, nhds

[loogle]

:search: Filter.Eventually.self_of_nhds, isOpen_setOf_eventually_nhds, and 521 more

[Etienne Marion]

First one

[Winston Yin (尹維晨)]

Thank you! How can I get better at loogle? I swear I’ve tried this…

[Eric Wieser]

And also

example {α : Type*} [TopologicalSpace α] (p : α → Prop) (x₀ : α)
    (h : ∀ᶠ x in nhds x₀, p x) : p x₀ :=
  mem_of_mem_nhds h

[Kevin Buzzard]

Winston Yin (尹維晨) said:

Thank you! How can I get better at loogle? I swear I’ve tried this…

For me the insight was that just giving a comma-separated list of the things you want to see in your declaration (without notation) was a very effective use.