Loogle!

Result

Found 4361 declarations mentioning nhds. Of these, only the first 200 are shown.

• nhds 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} [TopologicalSpace X] (x : X) : Filter X
• WeaklyLocallyCompactSpace.exists_compact_mem_nhds 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} {inst✝ : TopologicalSpace X} [self : WeaklyLocallyCompactSpace X] (x : X) : ∃ s, IsCompact s ∧ s ∈ nhds x
• WeaklyLocallyCompactSpace.mk 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} [TopologicalSpace X] (exists_compact_mem_nhds : ∀ (x : X), ∃ s, IsCompact s ∧ s ∈ nhds x) : WeaklyLocallyCompactSpace X
• LocallyCompactSpace.local_compact_nhds 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} {inst✝ : TopologicalSpace X} [self : LocallyCompactSpace X] (x : X) (n : Set X) : n ∈ nhds x → ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s
• LocallyCompactSpace.mk 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} [TopologicalSpace X] (local_compact_nhds : ∀ (x : X), ∀ n ∈ nhds x, ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s) : LocallyCompactSpace X
• LocallyCompactPair.exists_mem_nhds_isCompact_mapsTo 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} {Y : Type u_4} {inst✝ : TopologicalSpace X} {inst✝¹ : TopologicalSpace Y} [self : LocallyCompactPair X Y] {f : X → Y} {x : X} {s : Set Y} : Continuous f → s ∈ nhds (f x) → ∃ K ∈ nhds x, IsCompact K ∧ Set.MapsTo f K s
• LocallyCompactPair.mk 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] (exists_mem_nhds_isCompact_mapsTo : ∀ {f : X → Y} {x : X} {s : Set Y}, Continuous f → s ∈ nhds (f x) → ∃ K ∈ nhds x, IsCompact K ∧ Set.MapsTo f K s) : LocallyCompactPair X Y
• nhds_def 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_3} [TopologicalSpace X] (x : X) : nhds x = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, Filter.principal s
• limUnder_of_not_tendsto 📋 Mathlib.Topology.Basic
  {X : Type u} {α : Type u_1} [TopologicalSpace X] [hX : Nonempty X] {f : Filter α} {g : α → X} (h : ¬∃ x, Filter.Tendsto g f (nhds x)) : f.limUnder g = Classical.choice hX
• tendsto_nhds_limUnder 📋 Mathlib.Topology.Basic
  {X : Type u} {α : Type u_1} [TopologicalSpace X] {f : Filter α} {g : α → X} (h : ∃ x, Filter.Tendsto g f (nhds x)) : Filter.Tendsto g f (nhds (f.limUnder g))
• le_nhds_lim 📋 Mathlib.Topology.Basic
  {X : Type u} [TopologicalSpace X] {f : Filter X} (h : ∃ x, f ≤ nhds x) : f ≤ nhds f.lim
• nhds_neBot 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} : (nhds x).NeBot
• tendsto_const_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : Filter α} : Filter.Tendsto (fun x_1 => x) f (nhds x)
• Filter.Eventually.self_of_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhds x, p y) : p x
• isOpen_setOfPred_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
• isOpen_setOf_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhds x, p y}
• lift'_nhds_interior 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).lift' interior = nhds x
• nhds_bind_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} : (nhds x).bind nhds = nhds x
• tendsto_pure_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} (f : α → X) (a : α) : Filter.Tendsto f (pure a) (nhds (f a))
• TopologicalSpace.ext_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u_2} {t t' : TopologicalSpace X} : (∀ (x : X), nhds x = nhds x) → t = t'
• TopologicalSpace.ext_iff_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u_2} {t t' : TopologicalSpace X} : t = t' ↔ ∀ (x : X), nhds x = nhds x
• Filter.EventuallyEq.eq_of_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α} (h : f =ᶠ[nhds x] g) : f x = g x
• Filter.EventuallyEq.tendsto 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {l : Filter α} {f : α → X} (hf : f =ᶠ[l] fun x_1 => x) : Filter.Tendsto f l (nhds x)
• mem_of_mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : s ∈ nhds x → x ∈ s
• interior_eq_nhds' 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = {x | s ∈ nhds x}
• isOpen_singleton_iff_nhds_eq_pure 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : IsOpen {x} ↔ nhds x = pure x
• tendsto_nhds_of_eventually_eq 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {l : Filter α} {f : α → X} (h : ∀ᶠ (x' : α) in l, f x' = x) : Filter.Tendsto f l (nhds x)
• interior_setOfPred_eq 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : interior {x | p x} = {x | ∀ᶠ (y : X) in nhds x, p y}
• interior_setOf_eq 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {p : X → Prop} : interior {x | p x} = {x | ∀ᶠ (y : X) in nhds x, p y}
• pure_le_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] : pure ≤ nhds
• mem_interior_iff_mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ interior s ↔ s ∈ nhds x
• nhds_basis_opens 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).HasBasis (fun s => x ∈ s ∧ IsOpen s) fun s => s
• IsOpen.mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : s ∈ nhds x
• isOpen_iff_mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, s ∈ nhds x
• IsOpen.mem_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) : s ∈ nhds x ↔ x ∈ s
• Filter.Eventually.eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhds x, p y) : ∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x
• eventually_eventually_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhds x, p x
• frequently_frequently_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∃ᶠ (x' : X) in nhds x, ∃ᶠ (x'' : X) in nhds x', p x'') ↔ ∃ᶠ (x : X) in nhds x, p x
• Filter.Frequently.mem_closure 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : (∃ᶠ (x : X) in nhds x, x ∈ s) → x ∈ closure s
• interior_eq_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = {x | nhds x ≤ Filter.principal s}
• mem_closure_iff_frequently 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ∃ᶠ (x : X) in nhds x, x ∈ s
• nhds_basis_closeds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).HasBasis (fun s => x ∉ s ∧ IsClosed s) compl
• Dense.inter_nhds_nonempty 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s t : Set X} (hs : Dense s) (ht : t ∈ nhds x) : (s ∩ t).Nonempty
• IsOpen.eventually_mem 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : ∀ᶠ (x : X) in nhds x, x ∈ s
• Filter.Frequently.mem_of_closed 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (h : ∃ᶠ (x : X) in nhds x, x ∈ s) (hs : IsClosed s) : x ∈ s
• Filter.HasBasis.nhds_interior 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {ι : Sort v} {x : X} {p : ι → Prop} {s : ι → Set X} (h : (nhds x).HasBasis p s) : (nhds x).HasBasis p fun x => interior (s x)
• interior_mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : interior s ∈ nhds x ↔ s ∈ nhds x
• isClosed_iff_frequently 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in nhds x, y ∈ s) → x ∈ s
• isOpen_iff_eventually 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, y ∈ s
• nhds_basis_opens' 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).HasBasis (fun s => s ∈ nhds x ∧ IsOpen s) fun x => x
• tendsto_atBot_of_eventually_const 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u_2} [Preorder ι] {u : ι → X} {i₀ : ι} (h : ∀ i ≤ i₀, u i = x) : Filter.Tendsto u Filter.atBot (nhds x)
• tendsto_atTop_of_eventually_const 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {ι : Type u_2} [Preorder ι] {u : ι → X} {i₀ : ι} (h : ∀ i ≥ i₀, u i = x) : Filter.Tendsto u Filter.atTop (nhds x)
• Filter.EventuallyEq.eventuallyEq_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α} (h : f =ᶠ[nhds x] g) : ∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g
• eventually_eventuallyEq_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α} : (∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g) ↔ f =ᶠ[nhds x] g
• IsClosed.compl_mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsClosed s) (hx : x ∉ s) : sᶜ ∈ nhds x
• isOpen_iff_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, nhds x ≤ Filter.principal s
• nhdsWithin_neBot 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : (nhdsWithin x s).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ nhds x → (t ∩ s).Nonempty
• eventually_mem_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : (∀ᶠ (x' : X) in nhds x, s ∈ nhds x') ↔ s ∈ nhds x
• OrderTop.tendsto_atTop_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} [PartialOrder α] [OrderTop α] (f : α → X) : Filter.Tendsto f Filter.atTop (nhds (f ⊤))
• Filter.EventuallyLE.eventuallyLE_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [LE α] {f g : X → α} (h : f ≤ᶠ[nhds x] g) : ∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g
• eventually_eventuallyLE_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [LE α] {f g : X → α} : (∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g) ↔ f ≤ᶠ[nhds x] g
• subset_interior_iff_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s V : Set X} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ nhds x
• frequently_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∃ᶠ (y : X) in nhds x, p y) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ y ∈ U, p y
• mem_closure_of_frequently_of_tendsto 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} (h : ∃ᶠ (x : α) in b, f x ∈ s) (hf : Filter.Tendsto f b (nhds x)) : x ∈ closure s
• mem_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : s ∈ nhds x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t
• IsClosed.mem_of_frequently_of_tendsto 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} (hs : IsClosed s) (h : ∃ᶠ (x : α) in b, f x ∈ s) (hf : Filter.Tendsto f b (nhds x)) : x ∈ s
• eventually_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∀ᶠ (y : X) in nhds x, p y) ↔ ∃ t, (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t
• le_nhds_iff 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} : f ≤ nhds x ↔ ∀ (s : Set X), x ∈ s → IsOpen s → s ∈ f
• tendsto_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : α → X} {l : Filter α} : Filter.Tendsto f l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f ⁻¹' s ∈ l
• mem_closure_of_tendsto 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} [b.NeBot] (hf : Filter.Tendsto f b (nhds x)) (h : ∀ᶠ (x : α) in b, f x ∈ s) : x ∈ closure s
• IsClosed.mem_of_tendsto 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {s : Set X} {f : α → X} {b : Filter α} [b.NeBot] (hs : IsClosed s) (hf : Filter.Tendsto f b (nhds x)) (h : ∀ᶠ (x : α) in b, f x ∈ s) : x ∈ s
• nhds_le_of_le 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} {f : Filter X} (h : x ∈ s) (o : IsOpen s) (sf : Filter.principal s ≤ f) : nhds x ≤ f
• exists_open_set_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s U : Set X} (h : ∀ x ∈ s, U ∈ nhds x) : ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U
• tendsto_inf_principal_nhds_iff_of_forall_eq 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : α → X} {l : Filter α} {s : Set α} (h : ∀ a ∉ s, f a = x) : Filter.Tendsto f (l ⊓ Filter.principal s) (nhds x) ↔ Filter.Tendsto f l (nhds x)
• all_mem_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) (P : Set X → Prop) (hP : ∀ (s t : Set X), s ⊆ t → P s → P t) : (∀ s ∈ nhds x, P s) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → P s
• nhds_def' 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : nhds x = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), Filter.principal s
• tendsto_atTop_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} [Nonempty α] [SemilatticeSup α] {f : α → X} : Filter.Tendsto f Filter.atTop (nhds x) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ N, ∀ (n : α), N ≤ n → f n ∈ U
• exists_open_set_nhds' 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {s U : Set X} (h : U ∈ ⨆ x ∈ s, nhds x) : ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U
• all_mem_nhds_filter 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} (x : X) (f : Set X → Set α) (hf : ∀ (s t : Set X), s ⊆ t → f s ⊆ f t) (l : Filter α) : (∀ s ∈ nhds x, f s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f s ∈ l
• map_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : X → α} : Filter.map f (nhds x) = ⨅ s ∈ {s | x ∈ s ∧ IsOpen s}, Filter.principal (f '' s)
• ClusterPt.neBot 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} (h : ClusterPt x F) : (nhds x ⊓ F).NeBot
• ClusterPt.of_nhds_le 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} (H : nhds x ≤ f) : ClusterPt x f
• ClusterPt.frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ (y : X) in nhds x, p y) : ∃ᶠ (y : X) in F, p y
• ClusterPt.frequently' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} {p : X → Prop} (hx : ClusterPt x F) (hp : ∀ᶠ (y : X) in F, p y) : ∃ᶠ (y : X) in nhds x, p y
• Filter.Tendsto.mapClusterPt 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [F.NeBot] (h : Filter.Tendsto u F (nhds x)) : MapClusterPt x F u
• clusterPt_principal_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : ClusterPt x (Filter.principal s) ↔ ∃ᶠ (y : X) in nhds x, y ∈ s
• ClusterPt.of_le_nhds 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} (H : f ≤ nhds x) [f.NeBot] : ClusterPt x f
• ClusterPt.of_le_nhds' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} (H : f ≤ nhds x) (_hf : f.NeBot) : ClusterPt x f
• accPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhds x, y ≠ x ∧ y ∈ C
• MapClusterPt.frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} (h : MapClusterPt x F u) {p : X → Prop} (hp : ∀ᶠ (y : X) in nhds x, p y) : ∃ᶠ (a : α) in F, p (u a)
• clusterPt_principal_iff 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : ClusterPt x (Filter.principal s) ↔ ∀ U ∈ nhds x, (U ∩ s).Nonempty
• clusterPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ nhds x, ∃ᶠ (y : X) in F, y ∈ s
• clusterPt_iff_frequently' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ s ∈ F, ∃ᶠ (y : X) in nhds x, y ∈ s
• mem_closure_iff_nhds_ne_bot 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥
• clusterPt_iff_not_disjoint 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ¬Disjoint (nhds x) F
• mem_closure_iff_nhds 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ∀ t ∈ nhds x, (t ∩ s).Nonempty
• isClosed_iff_nhds 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s ↔ ∀ (x : X), (∀ U ∈ nhds x, (U ∩ s).Nonempty) → x ∈ s
• Filter.HasBasis.clusterPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : (nhds x).HasBasis p s) : ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in F, x ∈ s i
• Filter.HasBasis.clusterPt_iff_frequently' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X} (hx : F.HasBasis p s) : ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in nhds x, x ∈ s i
• mapClusterPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} : MapClusterPt x F u ↔ ∀ s ∈ nhds x, ∃ᶠ (a : α) in F, u a ∈ s
• clusterPt_iff_nonempty 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {F : Filter X} : ClusterPt x F ↔ ∀ ⦃U : Set X⦄, U ∈ nhds x → ∀ ⦃V : Set X⦄, V ∈ F → (U ∩ V).Nonempty
• mem_closure_iff_nhds_basis' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {ι : Sort w} {x : X} {t : Set X} {p : ι → Prop} {s : ι → Set X} (h : (nhds x).HasBasis p s) : x ∈ closure t ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty
• MapClusterPt.tendsto_comp 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (nhds x) (nhds y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u)
• Filter.HasBasis.mapClusterPt_iff_frequently 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} (hx : (nhds x).HasBasis p s) : MapClusterPt x F u ↔ ∀ (i : ι), p i → ∃ᶠ (a : α) in F, u a ∈ s i
• accPt_iff_nhds 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x
• mem_closure_of_mem_closure_union 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s₁ s₂ : Set X} (h : x ∈ closure (s₁ ∪ s₂)) (h₁ : s₁ᶜ ∈ nhds x) : x ∈ closure s₂
• isClosed_iff_forall_filter 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s ↔ ∀ (x : X) (F : Filter X), F.NeBot → F ≤ Filter.principal s → F ≤ nhds x → x ∈ s
• MapClusterPt.tendsto_comp' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X} [TopologicalSpace Y] {f : X → Y} {y : Y} (hf : Filter.Tendsto f (nhds x ⊓ Filter.map u F) (nhds y)) (hu : MapClusterPt x F u) : MapClusterPt y F (f ∘ u)
• Filter.HasBasis.clusterPt_iff 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {ιX : Sort u_3} {ιF : Sort u_4} {pX : ιX → Prop} {sX : ιX → Set X} {pF : ιF → Prop} {sF : ιF → Set X} {F : Filter X} (hX : (nhds x).HasBasis pX sX) (hF : F.HasBasis pF sF) : ClusterPt x F ↔ ∀ ⦃i : ιX⦄, pX i → ∀ ⦃j : ιF⦄, pF j → (sX i ∩ sF j).Nonempty
• mem_closure_iff_nhds_basis 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {ι : Sort w} {x : X} {t : Set X} {p : ι → Prop} {s : ι → Set X} (h : (nhds x).HasBasis p s) : x ∈ closure t ↔ ∀ (i : ι), p i → ∃ y ∈ t, y ∈ s i
• mem_closure_iff_comap_neBot 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ (Filter.comap Subtype.val (nhds x)).NeBot
• mem_closure_iff_nhds' 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ∀ t ∈ nhds x, ∃ y, ↑y ∈ t
• Filter.EventuallyEq.continuousAt 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {y : Y} (h : f =ᶠ[nhds x] fun x => y) : ContinuousAt f x
• Continuous.tendsto 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) : Filter.Tendsto f (nhds x) (nhds (f x))
• ContinuousAt.tendsto 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (h : ContinuousAt f x) : Filter.Tendsto f (nhds x) (nhds (f x))
• Continuous.tendsto' 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) (y : Y) (h : f x = y) : Filter.Tendsto f (nhds x) (nhds y)
• ContinuousAt.congr 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {g : X → Y} (hf : ContinuousAt f x) (h : f =ᶠ[nhds x] g) : ContinuousAt g x
• continuousAt_congr 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {g : X → Y} (h : f =ᶠ[nhds x] g) : ContinuousAt f x ↔ ContinuousAt g x
• DenseRange.mem_nhds 📋 Mathlib.Topology.Continuous
  {X : Type u_1} [TopologicalSpace X] {x : X} {α : Type u_4} {f : α → X} {s : Set X} (h : DenseRange f) (hs : s ∈ nhds x) : ∃ a, f a ∈ s
• tendsto_lift'_closure_nhds 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) : Filter.Tendsto f ((nhds x).lift' closure) ((nhds (f x)).lift' closure)
• ContinuousAt.eventually_mem 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (hf : ContinuousAt f x) {s : Set Y} (hs : s ∈ nhds (f x)) : ∀ᶠ (y : X) in nhds x, f y ∈ s
• ContinuousAt.preimage_mem_nhds 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {t : Set Y} (h : ContinuousAt f x) (ht : t ∈ nhds (f x)) : f ⁻¹' t ∈ nhds x
• continuousAt_def 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} : ContinuousAt f x ↔ ∀ A ∈ nhds (f x), f ⁻¹' A ∈ nhds x
• not_continuousAt_of_tendsto 📋 Mathlib.Topology.Continuous
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {l₁ : Filter X} {l₂ : Filter Y} {x : X} (hf : Filter.Tendsto f l₁ l₂) [l₁.NeBot] (hl₁ : l₁ ≤ nhds x) (hl₂ : Disjoint (nhds (f x)) l₂) : ¬ContinuousAt f x
• nhds_false 📋 Mathlib.Topology.Order
  : nhds False = ⊤
• nhds_true 📋 Mathlib.Topology.Order
  : nhds True = pure True
• nhds_discrete 📋 Mathlib.Topology.Order
  (α : Type u_3) [TopologicalSpace α] [DiscreteTopology α] : nhds = pure
• IndiscreteTopology.nhds_eq 📋 Mathlib.Topology.Order
  {α : Type u} [TopologicalSpace α] [IndiscreteTopology α] (a : α) : nhds a = ⊤
• discreteTopology_iff_nhds 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] : DiscreteTopology α ↔ ∀ (x : α), nhds x = pure x
• tendsto_nhds_true 📋 Mathlib.Topology.Order
  {α : Type u_1} {l : Filter α} {p : α → Prop} : Filter.Tendsto p l (nhds True) ↔ ∀ᶠ (x : α) in l, p x
• tendsto_nhds_Prop 📋 Mathlib.Topology.Order
  {α : Type u_1} {l : Filter α} {p : α → Prop} {q : Prop} : Filter.Tendsto p l (nhds q) ↔ q → ∀ᶠ (x : α) in l, p x
• nhds_nhdsAdjoint_of_ne 📋 Mathlib.Topology.Order
  {α : Type u} {a b : α} (f : Filter α) (h : b ≠ a) : nhds b = pure b
• nhds_nhdsAdjoint_same 📋 Mathlib.Topology.Order
  {α : Type u} (a : α) (f : Filter α) : nhds a = pure a ⊔ f
• discreteTopology_iff_singleton_mem_nhds 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] : DiscreteTopology α ↔ ∀ (x : α), {x} ∈ nhds x
• gc_nhds 📋 Mathlib.Topology.Order
  {α : Type u} (a : α) : GaloisConnection (nhdsAdjoint a) fun t => nhds a
• nhds_induced 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β) : nhds a = Filter.comap f (nhds (f a))
• continuous_nhdsAdjoint_dom 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type v} [TopologicalSpace β] {f : α → β} {a : α} {l : Filter α} : Continuous f ↔ Filter.Tendsto f l (nhds (f a))
• mem_nhds_discrete 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] [DiscreteTopology α] {x : α} {s : Set α} : s ∈ nhds x ↔ x ∈ s
• map_nhds_induced_eq 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} (a : α) : Filter.map f (nhds a) = nhdsWithin (f a) (Set.range f)
• map_nhds_induced_of_surjective 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type v} [T : TopologicalSpace α] {f : β → α} (hf : Function.Surjective f) (a : β) : Filter.map f (nhds a) = nhds (f a)
• induced_iff_nhds_eq 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type v} [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α) : tβ = TopologicalSpace.induced f tα ↔ ∀ (b : β), nhds b = Filter.comap f (nhds (f b))
• le_of_nhds_le_nhds 📋 Mathlib.Topology.Order
  {α : Type u_1} {t₁ t₂ : TopologicalSpace α} (h : ∀ (x : α), nhds x ≤ nhds x) : t₁ ≤ t₂
• nhds_mono 📋 Mathlib.Topology.Order
  {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) : nhds a ≤ nhds a
• nhds_nhdsAdjoint 📋 Mathlib.Topology.Order
  {α : Type u} [DecidableEq α] (a : α) (f : Filter α) : nhds = Function.update pure a (pure a ⊔ f)
• le_iff_nhds 📋 Mathlib.Topology.Order
  {α : Type u_1} (t t' : TopologicalSpace α) : t ≤ t' ↔ ∀ (x : α), nhds x ≤ nhds x
• preimage_nhds_coinduced 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {π : α → β} {s : Set β} {a : α} (hs : s ∈ nhds (π a)) : π ⁻¹' s ∈ nhds a
• map_nhds_induced_of_mem 📋 Mathlib.Topology.Order
  {α : Type u_1} {β : Type u_2} [t : TopologicalSpace β] {f : α → β} {a : α} (h : Set.range f ∈ nhds (f a)) : Filter.map f (nhds a) = nhds (f a)
• nhds_iInf 📋 Mathlib.Topology.Order
  {α : Type u} {ι : Sort u_1} {t : ι → TopologicalSpace α} {a : α} : nhds a = ⨅ i, nhds a
• nhds_inf 📋 Mathlib.Topology.Order
  {α : Type u} {t₁ t₂ : TopologicalSpace α} {a : α} : nhds a = nhds a ⊓ nhds a
• mem_nhds_induced 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type v} [T : TopologicalSpace α] (f : β → α) (a : β) (s : Set β) : s ∈ nhds a ↔ ∃ u ∈ nhds (f a), f ⁻¹' u ⊆ s
• TopologicalSpace.tendsto_nhds_generateFrom_iff 📋 Mathlib.Topology.Order
  {α : Type u} {β : Type u_1} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β} : Filter.Tendsto m f (nhds b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f
• TopologicalSpace.nhds_mkOfNhds_single 📋 Mathlib.Topology.Order
  {α : Type u} [DecidableEq α] {a₀ : α} {l : Filter α} (h : pure a₀ ≤ l) (b : α) : nhds b = Function.update pure a₀ l b
• nhds_top 📋 Mathlib.Topology.Order
  {α : Type u} {a : α} : nhds a = ⊤
• le_nhdsAdjoint_iff 📋 Mathlib.Topology.Order
  {α : Type u_1} (a : α) (f : Filter α) (t : TopologicalSpace α) : t ≤ nhdsAdjoint a f ↔ nhds a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen {b}
• le_nhdsAdjoint_iff' 📋 Mathlib.Topology.Order
  {α : Type u} {a : α} {f : Filter α} {t : TopologicalSpace α} : t ≤ nhdsAdjoint a f ↔ nhds a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → nhds b = pure b
• TopologicalSpace.nhds_mkOfNhds 📋 Mathlib.Topology.Order
  {α : Type u} (n : α → Filter α) (a : α) (h₀ : pure ≤ n) (h₁ : ∀ (a : α), ∀ s ∈ n a, ∀ᶠ (y : α) in n a, s ∈ n y) : nhds a = n a
• nhds_sInf 📋 Mathlib.Topology.Order
  {α : Type u} {s : Set (TopologicalSpace α)} {a : α} : nhds a = ⨅ t ∈ s, nhds a
• TopologicalSpace.nhds_mkOfNhds_of_hasBasis 📋 Mathlib.Topology.Order
  {α : Type u} {n : α → Filter α} {ι : α → Sort u_1} {p : (a : α) → ι a → Prop} {s : (a : α) → ι a → Set α} (hb : ∀ (a : α), (n a).HasBasis (p a) (s a)) (hpure : ∀ (a : α) (i : ι a), p a i → a ∈ s a i) (hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x) (a : α) : nhds a = n a
• TopologicalSpace.nhds_generateFrom 📋 Mathlib.Topology.Order
  {α : Type u} {g : Set (Set α)} {a : α} : nhds a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, Filter.principal s
• TopologicalSpace.nhds_mkOfNhds_filterBasis 📋 Mathlib.Topology.Order
  {α : Type u} (B : α → FilterBasis α) (a : α) (h₀ : ∀ (x : α), ∀ n ∈ B x, x ∈ n) (h₁ : ∀ (x : α), ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n) : nhds a = (B a).filter
• nhdsSet_singleton 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {x : X} : nhdsSet {x} = nhds x
• Filter.Eventually.eventually_nhdsSet 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhdsSet s, p y) : ∀ᶠ (y : X) in nhdsSet s, ∀ᶠ (x : X) in nhds y, p x
• nhdsSet_insert 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] (x : X) (s : Set X) : nhdsSet (insert x s) = nhds x ⊔ nhdsSet s
• nhds_le_nhdsSet 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {x : X} (h : x ∈ s) : nhds x ≤ nhdsSet s
• eventually_nhdsSet_iff_forall 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {p : X → Prop} : (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, p y
• tendsto_nhdsSet_of_tendsto_nhds 📋 Mathlib.Topology.NhdsSet
  {α : Type u_1} {X : Type u_2} [TopologicalSpace X] {s : Set X} {f : α → X} {l : Filter α} {x : X} (hx : x ∈ s) (hf : Filter.Tendsto f l (nhds x)) : Filter.Tendsto f l (nhdsSet s)
• nhdsSet_diagonal 📋 Mathlib.Topology.NhdsSet
  (X : Type u_4) [TopologicalSpace (X × X)] : nhdsSet (Set.diagonal X) = ⨆ x, nhds (x, x)
• mem_nhdsSet_iff_forall 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s t : Set X} : s ∈ nhdsSet t ↔ ∀ x ∈ t, s ∈ nhds x
• nhdsSet_le 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {f : Filter X} {s : Set X} : nhdsSet s ≤ f ↔ ∀ x ∈ s, nhds x ≤ f
• bUnion_mem_nhdsSet 📋 Mathlib.Topology.NhdsSet
  {X : Type u_2} [TopologicalSpace X] {s : Set X} {t : X → Set X} (h : ∀ x ∈ s, t x ∈ nhds x) : ⋃ x ∈ s, t x ∈ nhdsSet s
• IsOpenMap.range_mem_nhds 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (x : X) : Set.range f ∈ nhds (f x)
• Topology.IsInducing.nhds_eq_comap 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) (x : X) : nhds x = Filter.comap f (nhds (f x))
• Topology.IsOpenEmbedding.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) (x : X) : Filter.map f (nhds x) = nhds (f x)
• Topology.isInducing_iff_nhds 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] : Topology.IsInducing f ↔ ∀ (x : X), nhds x = Filter.comap f (nhds (f x))
• Topology.IsEmbedding.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsEmbedding f) (x : X) : Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)
• Topology.IsEmbedding.mk' 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (inj : Function.Injective f) (induced : ∀ (x : X), Filter.comap f (nhds (f x)) = nhds x) : Topology.IsEmbedding f
• Topology.IsInducing.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) (x : X) : Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)
• IsOpenMap.map_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {x : X} (hf' : ContinuousAt f x) : Filter.map f (nhds x) = nhds (f x)
• IsOpenMap.nhds_le 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) (x : X) : nhds (f x) ≤ Filter.map f (nhds x)
• IsOpenMap.of_nhds_le 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)) : IsOpenMap f
• isOpenMap_iff_nhds_le 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : IsOpenMap f ↔ ∀ (x : X), nhds (f x) ≤ Filter.map f (nhds x)
• Topology.IsClosedEmbedding.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] {g : ι → X} {l : Filter ι} {x : X} (hf : Topology.IsClosedEmbedding f) : Filter.Tendsto g l (nhds x) ↔ Filter.Tendsto (f ∘ g) l (nhds (f x))
• Topology.IsEmbedding.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
  {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : Topology.IsEmbedding g) : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y))
• Topology.IsInducing.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
  {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : Topology.IsInducing g) : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y))
• Topology.IsOpenEmbedding.tendsto_nhds_iff 📋 Mathlib.Topology.Maps.Basic
  {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace Z] {f : ι → Y} {l : Filter ι} {y : Y} (hg : Topology.IsOpenEmbedding g) : Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y))
• Topology.IsOpenEmbedding.tendsto_nhds_iff' 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsOpenEmbedding f) {l : Filter Z} {x : X} : Filter.Tendsto (g ∘ f) (nhds x) l ↔ Filter.Tendsto g (nhds (f x)) l
• IsClosedMap.comap_nhds_eq 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedMap f) (hf' : Continuous f) (y : Y) : Filter.comap f (nhds y) = nhdsSet (f ⁻¹' {y})
• IsOpenMap.image_mem_nhds 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsOpenMap f) {x : X} {s : Set X} (hx : s ∈ nhds x) : f '' s ∈ nhds (f x)
• Topology.IsEmbedding.map_nhds_of_mem 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : Topology.IsEmbedding f) (x : X) (h : Set.range f ∈ nhds (f x)) : Filter.map f (nhds x) = nhds (f x)
• Topology.IsInducing.map_nhds_of_mem 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) (x : X) (h : Set.range f ∈ nhds (f x)) : Filter.map f (nhds x) = nhds (f x)
• Topology.IsOpenEmbedding.image_mem_nhds 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Topology.IsOpenEmbedding f) {s : Set X} {x : X} : f '' s ∈ nhds (f x) ↔ s ∈ nhds x
• IsClosedMap.comap_nhds_le 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : IsClosedMap f → ∀ {y : Y}, Filter.comap f (nhds y) ≤ nhdsSet (f ⁻¹' {y})
• isClosedMap_iff_comap_nhds_le 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] : IsClosedMap f ↔ ∀ {y : Y}, Filter.comap f (nhds y) ≤ nhdsSet (f ⁻¹' {y})
• Topology.IsInducing.basis_nhds 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {ι : Type u_4} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] {p : ι → Prop} {s : ι → Set Y} (hf : Topology.IsInducing f) {x : X} (h_basis : (nhds (f x)).HasBasis p s) : (nhds x).HasBasis p (Set.preimage f ∘ s)
• Topology.IsInducing.image_mem_nhdsWithin 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace Y] [TopologicalSpace X] (hf : Topology.IsInducing f) {x : X} {s : Set X} (hs : s ∈ nhds x) : f '' s ∈ nhdsWithin (f x) (Set.range f)
• Topology.IsInducing.continuousAt_iff' 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [TopologicalSpace Y] [TopologicalSpace X] [TopologicalSpace Z] (hf : Topology.IsInducing f) {x : X} (h : Set.range f ∈ nhds (f x)) : ContinuousAt (g ∘ f) x ↔ ContinuousAt g (f x)
• IsClosedMap.eventually_nhds_fiber 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedMap f) {p : X → Prop} (y₀ : Y) (H : ∀ x₀ ∈ f ⁻¹' {y₀}, ∀ᶠ (x : X) in nhds x₀, p x) : ∀ᶠ (y : Y) in nhds y₀, ∀ x ∈ f ⁻¹' {y}, p x
• IsClosedMap.frequently_nhds_fiber 📋 Mathlib.Topology.Maps.Basic
  {X : Type u_1} {Y : Type u_2} {f : X → Y} [TopologicalSpace X] [TopologicalSpace Y] (hf : IsClosedMap f) {p : X → Prop} (y₀ : Y) (H : ∃ᶠ (y : Y) in nhds y₀, ∃ x ∈ f ⁻¹' {y}, p x) : ∃ x₀ ∈ f ⁻¹' {y₀}, ∃ᶠ (x : X) in nhds x₀, p x
• IsOpenQuotientMap.map_nhds_eq 📋 Mathlib.Topology.Maps.OpenQuotient
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : IsOpenQuotientMap f) (x : X) : Filter.map f (nhds x) = nhds (f x)
• Homeomorph.map_nhds_eq 📋 Mathlib.Topology.Homeomorph.Defs
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) (x : X) : Filter.map (⇑h) (nhds x) = nhds (h x)

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c