Loogle!

Result

Found 1543 declarations mentioning nhdsWithin. Of these, only the first 200 are shown.

• nhdsWithin 📋 Mathlib.Topology.Defs.Filter
  {X : Type u_1} [TopologicalSpace X] (x : X) (s : Set X) : Filter X
• nhdsWithin_mono 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) {s t : Set X} (h : s ⊆ t) : nhdsWithin x s ≤ nhdsWithin x t
• 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
• isOpen_singleton_iff_punctured_nhds 📋 Mathlib.Topology.Neighborhoods
  {X : Type u} [TopologicalSpace X] (x : X) : IsOpen {x} ↔ nhdsWithin x {x}ᶜ = ⊥
• mem_closure_iff_nhdsWithin_neBot 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ (nhdsWithin x s).NeBot
• notMem_closure_iff_nhdsWithin_eq_bot 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∉ closure s ↔ nhdsWithin x s = ⊥
• accPt_principal_iff_nhdsWithin 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : AccPt x (Filter.principal s) ↔ (nhdsWithin x (s \ {x})).NeBot
• not_isOpen_singleton 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : ¬IsOpen {x}
• dense_compl_singleton 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : Dense {x}ᶜ
• interior_singleton 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : interior {x} = ∅
• accPt_iff_frequently_nhdsNE 📋 Mathlib.Topology.ClusterPt
  {X : Type u_3} [TopologicalSpace X] {x : X} {C : Set X} : AccPt x (Filter.principal C) ↔ ∃ᶠ (y : X) in nhdsWithin x {x}ᶜ, y ∈ C
• closure_compl_singleton 📋 Mathlib.Topology.ClusterPt
  {X : Type u} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot] : closure {x}ᶜ = Set.univ
• 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)
• discreteTopology_iff_nhds_ne 📋 Mathlib.Topology.Order
  {α : Type u_1} [TopologicalSpace α] : DiscreteTopology α ↔ ∀ (x : α), nhdsWithin x {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.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)
• 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)
• map_fst_nhdsWithin 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.fst (nhdsWithin x (Prod.snd ⁻¹' {x.2})) = nhds x.1
• map_snd_nhdsWithin 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X × Y) : Filter.map Prod.snd (nhdsWithin x (Prod.fst ⁻¹' {x.1})) = nhds x.2
• nhdsWithin_prod_eq 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] (x : X) (y : Y) (s : Set X) (t : Set Y) : nhdsWithin (x, y) (s ×ˢ t) = nhdsWithin x s ×ˢ nhdsWithin y t
• Prod.instNeBotNhdsWithinIio 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Preorder X] [Preorder Y] {x : X × Y} [hx₁ : (nhdsWithin x.1 (Set.Iio x.1)).NeBot] [hx₂ : (nhdsWithin x.2 (Set.Iio x.2)).NeBot] : (nhdsWithin x (Set.Iio x)).NeBot
• Prod.instNeBotNhdsWithinIoi 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] [Preorder X] [Preorder Y] {x : X × Y} [hx₁ : (nhdsWithin x.1 (Set.Ioi x.1)).NeBot] [hx₂ : (nhdsWithin x.2 (Set.Ioi x.2)).NeBot] : (nhdsWithin x (Set.Ioi x)).NeBot
• mem_nhdsWithin_prod_iff 📋 Mathlib.Topology.Constructions.SumProd
  {X : Type u} {Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {s : Set (X × Y)} {tx : Set X} {ty : Set Y} : s ∈ nhdsWithin (x, y) (tx ×ˢ ty) ↔ ∃ u ∈ nhdsWithin x tx, ∃ v ∈ nhdsWithin y ty, u ×ˢ v ⊆ s
• comap_nhdsWithin_range 📋 Mathlib.Topology.Constructions
  {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (f : α → β) (y : β) : Filter.comap f (nhdsWithin y (Set.range f)) = Filter.comap f (nhds y)
• map_nhds_subtype_val 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s : Set X} (x : ↑s) : Filter.map Subtype.val (nhds x) = nhdsWithin (↑x) s
• OrderDual.instNeBotNhdsWithinIio 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] [Preorder X] {x : X} [(nhdsWithin x (Set.Ioi x)).NeBot] : (nhdsWithin (OrderDual.toDual x) (Set.Iio (OrderDual.toDual x))).NeBot
• OrderDual.instNeBotNhdsWithinIoi 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] [Preorder X] {x : X} [(nhdsWithin x (Set.Iio x)).NeBot] : (nhdsWithin (OrderDual.toDual x) (Set.Ioi (OrderDual.toDual x))).NeBot
• nhdsWithin_subtype_eq_bot_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {s t : Set X} {x : ↑s} : nhdsWithin x (Subtype.val ⁻¹' t) = ⊥ ↔ nhdsWithin (↑x) t ⊓ Filter.principal s = ⊥
• nhds_subtype_eq_comap_nhdsWithin 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] (s : Set X) (x : { x // x ∈ s }) : nhds x = Filter.comap Subtype.val (nhdsWithin (↑x) s)
• nhds_ne_subtype_neBot_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {S : Set X} {x : ↑S} : (nhdsWithin x {x}ᶜ).NeBot ↔ (nhdsWithin ↑x {↑x}ᶜ ⊓ Filter.principal S).NeBot
• nhds_ne_subtype_eq_bot_iff 📋 Mathlib.Topology.Constructions
  {X : Type u} [TopologicalSpace X] {S : Set X} {x : ↑S} : nhdsWithin x {x}ᶜ = ⊥ ↔ nhdsWithin ↑x {↑x}ᶜ ⊓ Filter.principal S = ⊥
• nhdsWithin_univ 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a Set.univ = nhds a
• self_mem_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : s ∈ nhdsWithin a s
• nhdsWithin_empty 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a ∅ = ⊥
• nhdsWithin_neBot_of_mem 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {x : α} (hx : x ∈ s) : (nhdsWithin x s).NeBot
• eventually_mem_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : ∀ᶠ (x : α) in nhdsWithin a s, x ∈ s
• DenseRange.nhdsWithin_neBot 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {f : ι → α} (h : DenseRange f) (x : α) : (nhdsWithin x (Set.range f)).NeBot
• nhdsWithin_singleton 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a {a} = pure a
• nhdsSetWithin_singleton 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} : nhdsSetWithin {x} s = nhdsWithin x s
• IsClosed.mem_of_nhdsWithin_neBot 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s : Set α} (hs : IsClosed s) {x : α} (hx : (nhdsWithin x s).NeBot) : x ∈ s
• nhdsWithin_le_nhds 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : nhdsWithin a s ≤ nhds a
• eventuallyEq_nhdsWithin_of_eqOn 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} (h : Set.EqOn f g s) : f =ᶠ[nhdsWithin a s] g
• eventually_nhdsWithin_of_eventually_nhds 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop} (h : ∀ᶠ (x : α) in nhds a, p x) : ∀ᶠ (x : α) in nhdsWithin a s, p x
• mem_nhdsWithin_inter_self 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : t ∈ nhdsWithin x (s ∩ t)
• mem_nhdsWithin_self_inter 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : s ∈ nhdsWithin x (s ∩ t)
• nhds_bind_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : ((nhds a).bind fun x => nhdsWithin x s) = nhdsWithin a s
• Set.EqOn.eventuallyEq_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} (h : Set.EqOn f g s) : f =ᶠ[nhdsWithin a s] g
• tendsto_const_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {l : Filter β} {s : Set α} {a : α} (ha : a ∈ s) : Filter.Tendsto (fun x => a) l (nhdsWithin a s)
• Filter.Eventually.self_of_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {p : α → Prop} {s : Set α} {x : α} (h : ∀ᶠ (y : α) in nhdsWithin x s, p y) (hx : x ∈ s) : p x
• eventually_nhdsWithin_of_forall 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} {p : α → Prop} (h : ∀ x ∈ s, p x) : ∀ᶠ (x : α) in nhdsWithin a s, p x
• nhdsWithin_eq_iff_eventuallyEq 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : nhdsWithin x s = nhdsWithin x t ↔ s =ᶠ[nhds x] t
• nhdsWithin_eq_iff_eventuallyEqSet 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : nhdsWithin x s = nhdsWithin x t ↔ s =ᶠ[nhds x] t
• tendsto_nhdsWithin_of_tendsto_nhds 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f (nhds a) l) : Filter.Tendsto f (nhdsWithin a s) l
• tendsto_nhds_of_tendsto_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f l (nhdsWithin a s)) : Filter.Tendsto f l (nhds a)
• IsOpen.nhdsWithin_eq 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} (h : IsOpen s) (ha : a ∈ s) : nhdsWithin a s = nhds a
• nhdsWithin_eq_nhds 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : nhdsWithin a s = nhds a ↔ s ∈ nhds a
• tendsto_nhdsWithin_range 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {f : β → α} : Filter.Tendsto f l (nhdsWithin a (Set.range f)) ↔ Filter.Tendsto f l (nhds a)
• mem_nhdsWithin_of_mem_nhds 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : α} (h : s ∈ nhds a) : s ∈ nhdsWithin a t
• eventually_mem_of_tendsto_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : β → α} {a : α} {s : Set α} {l : Filter β} (h : Filter.Tendsto f l (nhdsWithin a s)) : ∀ᶠ (i : β) in l, f i ∈ s
• Set.MapsTo.preimage_mem_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {s : Set α} {t : Set β} {x : α} (hst : Set.MapsTo f s t) : f ⁻¹' t ∈ nhdsWithin x s
• nhdsWithin_inter' 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) : nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ Filter.principal t
• pure_le_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} (ha : a ∈ s) : pure a ≤ nhdsWithin a s
• Filter.EventuallyEq.eq_of_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {f g : α → β} {a : α} (h : f =ᶠ[nhdsWithin a s] g) (hmem : a ∈ s) : f a = g a
• eventually_nhdsWithin_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (x : α) in nhdsWithin a s, p x) ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → p x
• eventually_nhds_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x
• mem_nhdsWithin_iff_eventuallyEq 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : t ∈ nhdsWithin x s ↔ s =ᶠ[nhds x] s ∩ t
• mem_nhdsWithin_iff_eventuallyEqSet 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : t ∈ nhdsWithin x s ↔ s =ᶠ[nhds x] s ∩ t
• nhdsWithin_iUnion 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} [Finite ι] (s : ι → Set α) (a : α) : nhdsWithin a (⋃ i, s i) = ⨆ i, nhdsWithin a (s i)
• nhdsWithin_insert 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) : nhdsWithin a (insert a s) = pure a ⊔ nhdsWithin a s
• eventually_eventually_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} {p : α → Prop} : (∀ᶠ (y : α) in nhdsWithin a s, ∀ᶠ (x : α) in nhdsWithin y s, p x) ↔ ∀ᶠ (x : α) in nhdsWithin a s, p x
• frequently_nhdsWithin_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} {p : α → Prop} : (∃ᶠ (x : α) in nhdsWithin z s, p x) ↔ ∃ᶠ (x : α) in nhds z, p x ∧ x ∈ s
• mem_of_mem_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (ha : a ∈ s) (ht : t ∈ nhdsWithin a s) : a ∈ t
• nhdsNE_sup_pure 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) : nhdsWithin a {a}ᶜ ⊔ pure a = nhds a
• nhdsWithin_inter 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) : nhdsWithin a (s ∩ t) = nhdsWithin a s ⊓ nhdsWithin a t
• nhdsWithin_union 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) (s t : Set α) : nhdsWithin a (s ∪ t) = nhdsWithin a s ⊔ nhdsWithin a t
• pure_sup_nhdsNE 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) : pure a ⊔ nhdsWithin a {a}ᶜ = nhds a
• inter_mem_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (s : Set α) {t : Set α} {a : α} (h : t ∈ nhds a) : s ∩ t ∈ nhdsWithin a s
• nhdsWithin_basis_open 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) (t : Set α) : (nhdsWithin a t).HasBasis (fun u => a ∈ u ∧ IsOpen u) fun u => u ∩ t
• nhdsWithin_hasBasis 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {ι : Sort u_3} {p : ι → Prop} {s : ι → Set α} {a : α} (h : (nhds a).HasBasis p s) (t : Set α) : (nhdsWithin a t).HasBasis p fun i => s i ∩ t
• nhdsWithin_restrict 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h₀ : a ∈ t) (h₁ : IsOpen t) : nhdsWithin a s = nhdsWithin a (s ∩ t)
• nhdsWithin_restrict' 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h : t ∈ nhds a) : nhdsWithin a s = nhdsWithin a (s ∩ t)
• nhdsWithin_inter_of_mem 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : s ∈ nhdsWithin a t) : nhdsWithin a (s ∩ t) = nhdsWithin a t
• nhdsWithin_inter_of_mem' 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : t ∈ nhdsWithin a s) : nhdsWithin a (s ∩ t) = nhdsWithin a s
• nhdsWithin_restrict'' 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} (s : Set α) {t : Set α} (h : t ∈ nhdsWithin a s) : nhdsWithin a s = nhdsWithin a (s ∩ t)
• tendsto_nhdsWithin_mono_left 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : α → β} {a : α} {s t : Set α} {l : Filter β} (hst : s ⊆ t) (h : Filter.Tendsto f (nhdsWithin a t) l) : Filter.Tendsto f (nhdsWithin a s) l
• tendsto_nhdsWithin_mono_right 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f : β → α} {l : Filter β} {a : α} {s t : Set α} (hst : s ⊆ t) (h : Filter.Tendsto f l (nhdsWithin a s)) : Filter.Tendsto f l (nhdsWithin a t)
• continuousAt_iff_punctured_nhds 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {a : α} : ContinuousAt f a ↔ Filter.Tendsto f (nhdsWithin a {a}ᶜ) (nhds (f a))
• nhdsWithin_le_of_mem 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : s ∈ nhdsWithin a t) : nhdsWithin a t ≤ nhdsWithin a s
• nhds_eq_nhdsWithin_sup_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (b : α) {I₁ I₂ : Set α} (hI : Set.univ = I₁ ∪ I₂) : nhds b = nhdsWithin b I₁ ⊔ nhdsWithin b I₂
• eventuallyEq_nhdsWithin_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} : f =ᶠ[nhdsWithin a s] g ↔ ∀ᶠ (x : α) in nhds a, x ∈ s → f x = g x
• eventually_mem_nhdsWithin_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {x : α} {s t : Set α} : (∀ᶠ (x' : α) in nhdsWithin x s, t ∈ nhdsWithin x' s) ↔ t ∈ nhdsWithin x s
• nhdsWithin_le_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : nhdsWithin x s ≤ nhdsWithin x t ↔ t ∈ nhdsWithin x s
• tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} (f : β → α) (h1 : Filter.Tendsto f l (nhds a)) (h2 : ∀ᶠ (x : β) in l, f x ∈ s) : Filter.Tendsto f l (nhdsWithin a s)
• diff_mem_nhdsWithin_compl 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} (hs : s ∈ nhds x) (t : Set α) : s \ t ∈ nhdsWithin x tᶜ
• sdiff_mem_nhdsWithin_compl 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {x : α} {s : Set α} (hs : s ∈ nhds x) (t : Set α) : s \ t ∈ nhdsWithin x tᶜ
• eventuallyEq_nhds_of_eventuallyEq_nhdsNE 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {a : α} (h₁ : f =ᶠ[nhdsWithin a {a}ᶜ] g) (h₂ : f a = g a) : f =ᶠ[nhds a] g
• mem_nhdsWithin_iff_eventually 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {x : α} : t ∈ nhdsWithin x s ↔ ∀ᶠ (y : α) in nhds x, y ∈ s → y ∈ t
• nhds_of_nhdsWithin_of_nhds 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : α} (h1 : s ∈ nhds a) (h2 : t ∈ nhdsWithin a s) : t ∈ nhds a
• tendsto_nhdsWithin_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {a : α} {l : Filter β} {s : Set α} {f : β → α} : Filter.Tendsto f l (nhdsWithin a s) ↔ Filter.Tendsto f l (nhds a) ∧ ∀ᶠ (n : β) in l, f n ∈ s
• instNeBotNhdsWithinUnivPi 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)} {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (s i)).NeBot] : (nhdsWithin x (Set.univ.pi s)).NeBot
• diff_mem_nhdsWithin_diff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {x : α} {s t : Set α} (hs : s ∈ nhdsWithin x t) (t' : Set α) : s \ t' ∈ nhdsWithin x (t \ t')
• insert_mem_nhdsWithin_insert 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} (h : t ∈ nhdsWithin a s) : insert a t ∈ nhdsWithin a (insert a s)
• sdiff_mem_nhdsWithin_sdiff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {x : α} {s t : Set α} (hs : s ∈ nhdsWithin x t) (t' : Set α) : s \ t' ∈ nhdsWithin x (t \ t')
• tendsto_nhdsWithin_congr 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {s : Set α} {a : α} {l : Filter β} (hfg : ∀ x ∈ s, f x = g x) (hf : Filter.Tendsto f (nhdsWithin a s) l) : Filter.Tendsto g (nhdsWithin a s) l
• insert_mem_nhds_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s : Set α} : insert a s ∈ nhds a ↔ s ∈ nhdsWithin a {a}ᶜ
• mem_nhdsWithin_insert 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s t : Set α} : t ∈ nhdsWithin a (insert a s) ↔ a ∈ t ∧ t ∈ nhdsWithin a s
• nhdsWithin_eq_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s t u : Set α} (h₀ : a ∈ s) (h₁ : IsOpen s) (h₂ : t ∩ s = u ∩ s) : nhdsWithin a t = nhdsWithin a u
• nhdsWithin_eq_nhdsWithin' 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a : α} {s t u : Set α} (hs : s ∈ nhds a) (h₂ : t ∩ s = u ∩ s) : nhdsWithin a t = nhdsWithin a u
• mem_nhdsWithin_iff_exists_mem_nhds_inter 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {t : Set α} {a : α} {s : Set α} : t ∈ nhdsWithin a s ↔ ∃ u ∈ nhds a, u ∩ s ⊆ t
• mem_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {t : Set α} {a : α} {s : Set α} : t ∈ nhdsWithin a s ↔ ∃ u, IsOpen u ∧ a ∈ u ∧ u ∩ s ⊆ t
• nhdsWithin_pi_neBot 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] {I : Set ι} {s : (i : ι) → Set (X i)} {x : (i : ι) → X i} : (nhdsWithin x (I.pi s)).NeBot ↔ ∀ i ∈ I, (nhdsWithin (x i) (s i)).NeBot
• Pi.instNeBotNhdsWithinIio 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [Nonempty ι] [(i : ι) → Preorder (X i)] {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (Set.Iio (x i))).NeBot] : (nhdsWithin x (Set.Iio x)).NeBot
• Pi.instNeBotNhdsWithinIoi 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [Nonempty ι] [(i : ι) → Preorder (X i)] {x : (i : ι) → X i} [∀ (i : ι), (nhdsWithin (x i) (Set.Ioi (x i))).NeBot] : (nhdsWithin x (Set.Ioi x)).NeBot
• mem_closure_ne_iff_frequently_within 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {z : α} {s : Set α} : z ∈ closure (s \ {z}) ↔ ∃ᶠ (x : α) in nhdsWithin z {z}ᶜ, x ∈ s
• nhdsWithin_sUnion 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {S : Set (Set α)} (hS : S.Finite) (a : α) : nhdsWithin a (⋃₀ S) = ⨆ s ∈ S, nhdsWithin a s
• inter_mem_nhdsWithin_inter 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {a b c d : Set α} {x : α} (h : a ∈ nhdsWithin x b) (h' : c ∈ nhdsWithin x d) : a ∩ c ∈ nhdsWithin x (b ∩ d)
• punctured_nhds_eq_nhdsWithin_sup_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {x : α} : nhdsWithin x {x}ᶜ = nhdsWithin x (Set.Iio x) ⊔ nhdsWithin x (Set.Ioi x)
• nhdsWithin_pi_univ_eq 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] [Finite ι] (s : (i : ι) → Set (X i)) (x : (i : ι) → X i) : nhdsWithin x (Set.univ.pi s) = ⨅ i, Filter.comap (fun x => x i) (nhdsWithin (x i) (s i))
• union_mem_nhds_of_mem_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {b : α} {I₁ I₂ : Set α} (h : Set.univ = I₁ ∪ I₂) {L : Set α} (hL : L ∈ nhdsWithin b I₁) {R : Set α} (hR : R ∈ nhdsWithin b I₂) : L ∪ R ∈ nhds b
• eventually_nhds_subtype_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop) : (∀ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∀ᶠ (x : α) in nhdsWithin (↑a) s, P x
• frequently_nhds_subtype_iff 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : ↑s) (P : α → Prop) : (∃ᶠ (x : ↑s) in nhds a, P ↑x) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) s, P x
• tendsto_nhdsWithin_iff_subtype 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {a : α} (h : a ∈ s) (f : α → β) (l : Filter β) : Filter.Tendsto f (nhdsWithin a s) l ↔ Filter.Tendsto (s.domRestrict f) (nhds ⟨a, h⟩) l
• nhdsWithin_pi_eq_bot 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] {I : Set ι} {s : (i : ι) → Set (X i)} {x : (i : ι) → X i} : nhdsWithin x (I.pi s) = ⊥ ↔ ∃ i ∈ I, nhdsWithin (x i) (s i) = ⊥
• nhdsWithin_biUnion 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {ι : Type u_3} {I : Set ι} (hI : I.Finite) (s : ι → Set α) (a : α) : nhdsWithin a (⋃ i ∈ I, s i) = ⨆ i ∈ I, nhdsWithin a (s i)
• Filter.Tendsto.if_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {p : α → Prop} [DecidablePred p] {a : α} {s : Set α} {l : Filter β} (h₀ : Filter.Tendsto f (nhdsWithin a (s ∩ {x | p x})) l) (h₁ : Filter.Tendsto g (nhdsWithin a (s ∩ {x | ¬p x})) l) : Filter.Tendsto (fun x => if p x then f x else g x) (nhdsWithin a s) l
• Filter.Tendsto.piecewise_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {f g : α → β} {t : Set α} [(x : α) → Decidable (x ∈ t)] {a : α} {s : Set α} {l : Filter β} (h₀ : Filter.Tendsto f (nhdsWithin a (s ∩ t)) l) (h₁ : Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) l) : Filter.Tendsto (t.piecewise f g) (nhdsWithin a s) l
• preimage_coe_mem_nhds_subtype 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} {a : ↑s} : Subtype.val ⁻¹' t ∈ nhds a ↔ t ∈ nhdsWithin (↑a) s
• nhdsWithin_eq_map_subtype_coe 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : α} (h : a ∈ s) : nhdsWithin a s = Filter.map Subtype.val (nhds ⟨a, h⟩)
• mem_nhds_subtype_iff_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : ↑s} {t : Set ↑s} : t ∈ nhds a ↔ Subtype.val '' t ∈ nhdsWithin (↑a) s
• preimage_nhdsWithin_coinduced' 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {X : α → β} {s : Set β} {t : Set α} {a : α} (h : a ∈ t) (hs : s ∈ nhds (X a)) : X ⁻¹' s ∈ nhdsWithin a t
• nhdsWithin_eq 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (a : α) (s : Set α) : nhdsWithin a s = ⨅ t ∈ {t | a ∈ t ∧ IsOpen t}, Filter.principal (t ∩ s)
• nhdsWithin_prod 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s u : Set α} {t v : Set β} {a : α} {b : β} (hu : u ∈ nhdsWithin a s) (hv : v ∈ nhdsWithin b t) : u ×ˢ v ∈ nhdsWithin (a, b) (s ×ˢ t)
• nhdsWithin_pi_eq' 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] {I : Set ι} (hI : I.Finite) (s : (i : ι) → Set (X i)) (x : (i : ι) → X i) : nhdsWithin x (I.pi s) = ⨅ i, Filter.comap (fun x => x i) (nhds (x i) ⊓ ⨅ (_ : i ∈ I), Filter.principal (s i))
• map_nhdsWithin 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] (f : α → β) (a : α) (s : Set α) : Filter.map f (nhdsWithin a s) = ⨅ t ∈ {t | a ∈ t ∧ IsOpen t}, Filter.principal (f '' (t ∩ s))
• clusterPt_principal_subtype_iff_frequently 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s t : Set α} (hst : s ⊆ t) {J : Set ↑s} {a : ↑s} : ClusterPt a (Filter.principal J) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) t, ∃ (h : x ∈ s), ⟨x, h⟩ ∈ J
• nhds_of_Ici_Iic 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] {b : α} {L : Set α} (hL : L ∈ nhdsWithin b (Set.Iic b)) {R : Set α} (hR : R ∈ nhdsWithin b (Set.Ici b)) : L ∩ Set.Iic b ∪ R ∩ Set.Ici b ∈ nhds b
• nhdsWithin_subtype 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] (s : Set α) (a : { x // x ∈ s }) (t : Set { x // x ∈ s }) : nhdsWithin a t = Filter.comap Subtype.val (nhdsWithin (↑a) (Subtype.val '' t))
• nhdsWithin_pi_eq 📋 Mathlib.Topology.NhdsWithin
  {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → TopologicalSpace (X i)] {I : Set ι} (hI : I.Finite) (s : (i : ι) → Set (X i)) (x : (i : ι) → X i) : nhdsWithin x (I.pi s) = (⨅ i ∈ I, Filter.comap (fun x => x i) (nhdsWithin (x i) (s i))) ⊓ ⨅ i, ⨅ (_ : i ∉ I), Filter.comap (fun x => x i) (nhds (x i))
• mem_nhdsWithin_subtype 📋 Mathlib.Topology.NhdsWithin
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {a : { x // x ∈ s }} {t u : Set { x // x ∈ s }} : t ∈ nhdsWithin a u ↔ t ∈ Filter.comap Subtype.val (nhdsWithin (↑a) (Subtype.val '' u))
• ContinuousWithinAt.tendsto 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) : Filter.Tendsto f (nhdsWithin x s) (nhds (f x))
• ContinuousWithinAt.tendsto_nhdsWithin_image 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) : Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) (f '' s))
• Topology.IsEmbedding.map_nhdsWithin_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsEmbedding f) (s : Set α) (x : α) : Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)
• Topology.IsInducing.map_nhdsWithin_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsInducing f) (s : Set α) (x : α) : Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)
• Topology.IsOpenEmbedding.map_nhdsWithin_preimage_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Topology.IsOpenEmbedding f) (s : Set β) (x : α) : Filter.map f (nhdsWithin x (f ⁻¹' s)) = nhdsWithin (f x) s
• ContinuousWithinAt.mono_of_mem_nhdsWithin 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s t : Set α} {x : α} (h : ContinuousWithinAt f t x) (hs : t ∈ nhdsWithin x s) : ContinuousWithinAt f s x
• ContinuousWithinAt.tendsto_nhdsWithin 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : Set.MapsTo f s t) : Filter.Tendsto f (nhdsWithin x s) (nhdsWithin (f x) t)
• ContinuousWithinAt.congr_of_eventuallyEq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[nhdsWithin x s] f) (hx : g x = f x) : ContinuousWithinAt g s x
• ContinuousWithinAt.congr_of_eventuallyEq_insert 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[nhdsWithin x (insert x s)] f) : ContinuousWithinAt g s x
• Filter.EventuallyEq.congr_continuousWithinAt 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} {x : α} (h : f =ᶠ[nhdsWithin x s] g) (hx : f x = g x) : ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
• ContinuousWithinAt.congr_of_eventuallyEq_of_mem 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} {x : α} (h : ContinuousWithinAt f s x) (h₁ : g =ᶠ[nhdsWithin x s] f) (hx : x ∈ s) : ContinuousWithinAt g s x
• Filter.EventuallyEq.congr_continuousWithinAt_of_insert 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} {x : α} (h : f =ᶠ[nhdsWithin x (insert x s)] g) : ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
• Filter.EventuallyEq.congr_continuousWithinAt_of_mem 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s : Set α} {x : α} (h : f =ᶠ[nhdsWithin x s] g) (hx : x ∈ s) : ContinuousWithinAt f s x ↔ ContinuousWithinAt g s x
• continuousWithinAt_inter' 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s t : Set α} {x : α} (h : t ∈ nhdsWithin x s) : ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x
• nhdsWithin_le_comap 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} (ctsf : ContinuousWithinAt f s x) : nhdsWithin x s ≤ Filter.comap f (nhdsWithin (f x) (f '' s))
• ContinuousWithinAt.preimage_mem_nhdsWithin 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : t ∈ nhds (f x)) : f ⁻¹' t ∈ nhdsWithin x s
• Function.LeftInverse.map_nhds_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} {x : β} (h : Function.LeftInverse f g) (hf : ContinuousWithinAt f (Set.range g) (g x)) (hg : ContinuousAt g x) : Filter.map g (nhds x) = nhdsWithin (g x) (Set.range g)
• ContinuousWithinAt.preimage_mem_nhdsWithin' 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} {t : Set β} (h : ContinuousWithinAt f s x) (ht : t ∈ nhdsWithin (f x) (f '' s)) : f ⁻¹' t ∈ nhdsWithin x s
• ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (h : f ⁻¹' t ∈ nhdsWithin x s) : ContinuousWithinAt (g ∘ f) s x
• ContinuousWithinAt.preimage_mem_nhdsWithin'' 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {y : β} {s t : Set β} (h : ContinuousWithinAt f (f ⁻¹' s) x) (ht : t ∈ nhdsWithin y s) (hxy : y = f x) : f ⁻¹' t ∈ nhdsWithin x (f ⁻¹' s)
• ContinuousWithinAt.comp_of_mem_nhdsWithin_image 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} (hg : ContinuousWithinAt g t (f x)) (hf : ContinuousWithinAt f s x) (hs : t ∈ nhdsWithin (f x) (f '' s)) : ContinuousWithinAt (g ∘ f) s x
• Set.LeftInvOn.map_nhdsWithin_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : β → α} {x : β} {s : Set β} (h : Set.LeftInvOn f g s) (hx : f (g x) = x) (hf : ContinuousWithinAt f (g '' s) (g x)) (hg : ContinuousWithinAt g s x) : Filter.map g (nhdsWithin x s) = nhdsWithin (g x) (g '' s)
• continuousOn_to_generateFrom_iff 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} [TopologicalSpace α] {s : Set α} {β : Type u_5} {T : Set (Set β)} {f : α → β} : ContinuousOn f s ↔ ∀ x ∈ s, ∀ t ∈ T, f x ∈ t → f ⁻¹' t ∈ nhdsWithin x s
• ContinuousWithinAt.comp_of_mem_nhdsWithin_image_of_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (hs : t ∈ nhdsWithin y (f '' s)) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x
• ContinuousWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq 📋 Mathlib.Topology.ContinuousOn
  {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β} (hg : ContinuousWithinAt g t y) (hf : ContinuousWithinAt f s x) (h : f ⁻¹' t ∈ nhdsWithin x s) (hy : f x = y) : ContinuousWithinAt (g ∘ f) s x
• TopologicalSpace.isCountablyGenerated_nhdsWithin 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] (x : α) [(nhds x).IsCountablyGenerated] (s : Set α) : (nhdsWithin x s).IsCountablyGenerated
• TopologicalSpace.countable_cover_nhdsWithin 📋 Mathlib.Topology.Bases
  {α : Type u} [t : TopologicalSpace α] [SecondCountableTopology α] {f : α → Set α} {s : Set α} (hf : ∀ x ∈ s, f x ∈ nhdsWithin x s) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
• exists_nhds_ne_neBot 📋 Mathlib.Topology.Compactness.Compact
  (X : Type u_2) [TopologicalSpace X] [CompactSpace X] [Infinite X] : ∃ z, (nhdsWithin z {z}ᶜ).NeBot
• exists_nhds_ne_inf_principal_neBot 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (hs' : s.Infinite) : ∃ z ∈ s, (nhdsWithin z {z}ᶜ ⊓ Filter.principal s).NeBot
• IsCompact.compl_mem_sets_of_nhdsWithin 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {f : Filter X} (hf : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, tᶜ ∈ f) : sᶜ ∈ f
• IsCompact.induction_on 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) {p : Set X → Prop} (he : p ∅) (hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s) (hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)) (hnhds : ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, p t) : p s
• IsCompact.elim_nhdsWithin_subcover 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : X → Set X) (hU : ∀ x ∈ s, U x ∈ nhdsWithin x s) : ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
• IsCompact.elim_nhdsWithin_subcover' 📋 Mathlib.Topology.Compactness.Compact
  {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsCompact s) (U : (x : X) → x ∈ s → Set X) (hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ nhdsWithin x s) : ∃ t, s ⊆ ⋃ x ∈ t, U ↑x ⋯
• LocallyFinite.nhdsWithin_iUnion 📋 Mathlib.Topology.LocallyFinite
  {ι : Type u_1} {X : Type u_4} [TopologicalSpace X] {f : ι → Set X} (hf : LocallyFinite f) (a : X) : nhdsWithin a (⋃ i, f i) = ⨆ i, nhdsWithin a (f i)
• countable_cover_nhdsWithin_of_sigmaCompact 📋 Mathlib.Topology.Compactness.SigmaCompact
  {X : Type u_1} [TopologicalSpace X] [SigmaCompactSpace X] {f : X → Set X} {s : Set X} (hs : IsClosed s) (hf : ∀ x ∈ s, f x ∈ nhdsWithin x s) : ∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
• inseparable_of_nhdsWithin_eq 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (hx : x ∈ s) (hy : y ∈ s) (h : nhdsWithin x s = nhdsWithin y s) : Inseparable x y
• specializes_of_nhdsWithin 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] {x y : X} {s : Set X} (h₁ : nhdsWithin x s ≤ nhdsWithin y s) (h₂ : x ∈ s) : x ⤳ y
• SeparationQuotient.map_mk_nhdsWithin_preimage 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] (s : Set (SeparationQuotient X)) (x : X) : Filter.map SeparationQuotient.mk (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) = nhdsWithin (SeparationQuotient.mk x) s
• SeparationQuotient.tendsto_lift_nhdsWithin_mk 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {α : Type u_4} [TopologicalSpace X] {x : X} {f : X → α} {hf : ∀ (x y : X), Inseparable x y → f x = f y} {s : Set (SeparationQuotient X)} {l : Filter α} : Filter.Tendsto (SeparationQuotient.lift f hf) (nhdsWithin (SeparationQuotient.mk x) s) l ↔ Filter.Tendsto f (nhdsWithin x (SeparationQuotient.mk ⁻¹' s)) l
• SeparationQuotient.tendsto_lift₂_nhdsWithin 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} {Y : Type u_2} {α : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y → α} {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d} {x : X} {y : Y} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {l : Filter α} : Filter.Tendsto (Function.uncurry (SeparationQuotient.lift₂ f hf)) (nhdsWithin (SeparationQuotient.mk x, SeparationQuotient.mk y) s) l ↔ Filter.Tendsto (Function.uncurry f) (nhdsWithin (x, y) (Prod.map SeparationQuotient.mk SeparationQuotient.mk ⁻¹' s)) l
• continuousAt_update_same 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} [DecidableEq α] {y : β} : ContinuousAt (Function.update f x y) x ↔ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds y)
• continuousWithinAt_update_same 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} {x : α} [DecidableEq α] {y : β} : ContinuousWithinAt (Function.update f x y) s x ↔ Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhds y)
• continuous_if' 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {p : α → Prop} [(a : α) → Decidable (p a)] (hpf : ∀ a ∈ frontier {x | p x}, Filter.Tendsto f (nhdsWithin a {x | p x}) (nhds (if p a then f a else g a))) (hpg : ∀ a ∈ frontier {x | p x}, Filter.Tendsto g (nhdsWithin a {x | ¬p x}) (nhds (if p a then f a else g a))) (hf : ContinuousOn f {x | p x}) (hg : ContinuousOn g {x | ¬p x}) : Continuous fun a => if p a then f a else g a
• ContinuousOn.piecewise' 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f g : α → β} {s t : Set α} [(a : α) → Decidable (a ∈ t)] (hpf : ∀ a ∈ s ∩ frontier t, Filter.Tendsto f (nhdsWithin a (s ∩ t)) (nhds (t.piecewise f g a))) (hpg : ∀ a ∈ s ∩ frontier t, Filter.Tendsto g (nhdsWithin a (s ∩ tᶜ)) (nhds (t.piecewise f g a))) (hf : ContinuousOn f (s ∩ t)) (hg : ContinuousOn g (s ∩ tᶜ)) : ContinuousOn (t.piecewise f g) s
• ContinuousOn.if' 📋 Mathlib.Topology.Piecewise
  {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {p : α → Prop} {f g : α → β} [(a : α) → Decidable (p a)] (hpf : ∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto f (nhdsWithin a (s ∩ {a | p a})) (nhds (if p a then f a else g a))) (hpg : ∀ a ∈ s ∩ frontier {a | p a}, Filter.Tendsto g (nhdsWithin a (s ∩ {a | ¬p a})) (nhds (if p a then f a else g a))) (hf : ContinuousOn f (s ∩ {a | p a})) (hg : ContinuousOn g (s ∩ {a | ¬p a})) : ContinuousOn (fun a => if p a then f a else g a) s
• eventually_ne_nhdsWithin 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {a b : X} {s : Set X} (h : a ≠ b) : ∀ᶠ (x : X) in nhdsWithin a s, x ≠ b
• nhdsWithin_of_mem_discrete 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsDiscrete s) {x : X} (hx : x ∈ s) : nhdsWithin x s = pure x
• nhdsWithin_insert_of_ne 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} {s : Set X} (hxy : x ≠ y) : nhdsWithin x (insert y s) = nhdsWithin x s
• isOpen_setOfPred_eventually_nhdsWithin 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y}
• isOpen_setOf_eventually_nhdsWithin 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {p : X → Prop} : IsOpen {x | ∀ᶠ (y : X) in nhdsWithin x {x}ᶜ, p y}
• Ne.nhdsWithin_compl_singleton 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ≠ y) : nhdsWithin x {y}ᶜ = nhds x
• nhdsNE_le_cofinite 📋 Mathlib.Topology.Separation.Basic
  {α : Type u_3} [TopologicalSpace α] [T1Space α] (a : α) : nhdsWithin a {a}ᶜ ≤ Filter.cofinite
• singleton_mem_nhdsWithin_of_mem_discrete 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} (hs : IsDiscrete s) {x : X} (hx : x ∈ s) : {x} ∈ nhdsWithin x s
• Ne.nhdsWithin_diff_singleton 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ≠ y) (s : Set X) : nhdsWithin x (s \ {y}) = nhdsWithin x s
• Ne.nhdsWithin_sdiff_singleton 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} (h : x ≠ y) (s : Set X) : nhdsWithin x (s \ {y}) = nhdsWithin x s
• eventually_nhdsWithin_eventually_nhds_iff_of_isOpen 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] {s : Set X} {a : X} {p : X → Prop} (hs : IsOpen s) : (∀ᶠ (y : X) in nhdsWithin a s, ∀ᶠ (x : X) in nhds y, p x) ↔ ∀ᶠ (x : X) in nhdsWithin a s, p x
• infinite_of_mem_nhds 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_3} [TopologicalSpace X] [T1Space X] (x : X) [hx : (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : s ∈ nhds x) : s.Infinite
• Function.update_eventuallyEq_nhdsNE 📋 Mathlib.Topology.Separation.Basic
  {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [T1Space α] [DecidableEq α] (f : α → β) (a a' : α) (b : β) : Function.update f a b =ᶠ[nhdsWithin a' {a'}ᶜ] f
• insert_mem_nhdsWithin_of_subset_insert 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] {x y : X} {s t : Set X} (hu : t ⊆ insert y s) : insert x s ∈ nhdsWithin x t
• Dense.diff_finite 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : Dense s) {t : Set X} (ht : t.Finite) : Dense (s \ t)
• Dense.sdiff_finite 📋 Mathlib.Topology.Separation.Basic
  {X : Type u_1} [TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X} (hs : Dense s) {t : Set X} (ht : t.Finite) : Dense (s \ t)

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 69fae59