Neighborhoods in topological spaces

Each point x of X gets a neighborhood filter 𝓝 x.

Tags

neighborhood

theorem nhds_def' {X : Type u} [TopologicalSpace X] (x : X) : nhds x = ⨅ (s : Set X), ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), Filter.principal s

theorem nhds_basis_opens {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∈ s ∧ IsOpen s) fun (s : Set X) => s

The open sets containing x are a basis for the neighborhood filter. See nhds_basis_opens' for a variant using open neighborhoods instead.

theorem nhds_basis_closeds {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => x ∉ s ∧ IsClosed s) compl

@[simp]

theorem lift'_nhds_interior {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).lift' interior = nhds x

theorem Filter.HasBasis.nhds_interior {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)

theorem le_nhds_iff {X : Type u} [TopologicalSpace X] {x : X} {f : Filter X} : f ≤ nhds x ↔ ∀ (s : Set X), x ∈ s → IsOpen s → s ∈ f

A filter lies below the neighborhood filter at x iff it contains every open set around x.

theorem nhds_le_of_le {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

To show a filter is above the neighborhood filter at x, it suffices to show that it is above the principal filter of some open set s containing x.

theorem mem_nhds_iff {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : s ∈ nhds x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t

theorem eventually_nhds_iff {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} : (∀ᶠ (y : X) in nhds x, p y) ↔ ∃ (t : Set X), (∀ y ∈ t, p y) ∧ IsOpen t ∧ x ∈ t

A predicate is true in a neighborhood of x iff it is true for all the points in an open set containing x.

theorem frequently_nhds_iff {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

theorem mem_interior_iff_mem_nhds {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ interior s ↔ s ∈ nhds x

theorem map_nhds {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : X → α} : Filter.map f (nhds x) = ⨅ s ∈ {s : Set X | x ∈ s ∧ IsOpen s}, Filter.principal (f '' s)

theorem mem_of_mem_nhds {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : s ∈ nhds x → x ∈ s

theorem Filter.Eventually.self_of_nhds {X : Type u} [TopologicalSpace X] {x : X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhds x, p y) : p x

If a predicate is true in a neighborhood of x, then it is true for x.

theorem IsOpen.mem_nhds {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : s ∈ nhds x

theorem IsOpen.mem_nhds_iff {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) : s ∈ nhds x ↔ x ∈ s

theorem IsClosed.compl_mem_nhds {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsClosed s) (hx : x ∉ s) : sᶜ ∈ nhds x

theorem IsOpen.eventually_mem {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (hs : IsOpen s) (hx : x ∈ s) : ∀ᶠ (x : X) in nhds x, x ∈ s

theorem nhds_basis_opens' {X : Type u} [TopologicalSpace X] (x : X) : (nhds x).HasBasis (fun (s : Set X) => s ∈ nhds x ∧ IsOpen s) fun (x : Set X) => x

The open neighborhoods of x are a basis for the neighborhood filter. See nhds_basis_opens for a variant using open sets around x instead.

theorem exists_open_set_nhds {X : Type u} [TopologicalSpace X] {s U : Set X} (h : ∀ x ∈ s, U ∈ nhds x) : ∃ (V : Set X), s ⊆ V ∧ IsOpen V ∧ V ⊆ U

If U is a neighborhood of each point of a set s then it is a neighborhood of s: it contains an open set containing s.

theorem exists_open_set_nhds' {X : Type u} [TopologicalSpace X] {s U : Set X} (h : U ∈ ⨆ x ∈ s, nhds x) : ∃ (V : Set X), s ⊆ V ∧ IsOpen V ∧ V ⊆ U

If U is a neighborhood of each point of a set s then it is a neighborhood of s: it contains an open set containing s.

theorem Filter.Eventually.eventually_nhds {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

If a predicate is true in a neighbourhood of x, then for y sufficiently close to x this predicate is true in a neighbourhood of y.

@[simp]

theorem eventually_eventually_nhds {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

@[simp]

theorem frequently_frequently_nhds {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

@[simp]

theorem eventually_mem_nhds_iff {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : (∀ᶠ (x' : X) in nhds x, s ∈ nhds x') ↔ s ∈ nhds x

@[simp]

theorem nhds_bind_nhds {X : Type u} [TopologicalSpace X] {x : X} : (nhds x).bind nhds = nhds x

@[simp]

theorem eventually_eventuallyEq_nhds {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

theorem Filter.EventuallyEq.eq_of_nhds {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α} (h : f =ᶠ[nhds x] g) : f x = g x

@[simp]

theorem eventually_eventuallyLE_nhds {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

theorem Filter.EventuallyEq.eventuallyEq_nhds {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

If two functions are equal in a neighbourhood of x, then for y sufficiently close to x these functions are equal in a neighbourhood of y.

theorem Filter.EventuallyLE.eventuallyLE_nhds {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

If f x ≤ g x in a neighbourhood of x, then for y sufficiently close to x we have f x ≤ g x in a neighbourhood of y.

theorem all_mem_nhds {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

theorem all_mem_nhds_filter {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

theorem tendsto_nhds {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

theorem tendsto_atTop_nhds {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

theorem tendsto_const_nhds {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {f : Filter α} : Filter.Tendsto (fun (x_1 : α) => x) f (nhds x)

theorem tendsto_atTop_of_eventually_const {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)

theorem tendsto_atBot_of_eventually_const {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)

theorem pure_le_nhds {X : Type u} [TopologicalSpace X] : pure ≤ nhds

theorem tendsto_pure_nhds {X : Type u} [TopologicalSpace X] {α : Type u_1} (f : α → X) (a : α) : Filter.Tendsto f (pure a) (nhds (f a))

theorem OrderTop.tendsto_atTop_nhds {X : Type u} [TopologicalSpace X] {α : Type u_1} [PartialOrder α] [OrderTop α] (f : α → X) : Filter.Tendsto f Filter.atTop (nhds (f ⊤))

@[simp]

instance nhds_neBot {X : Type u} [TopologicalSpace X] {x : X} : (nhds x).NeBot

theorem tendsto_nhds_of_eventually_eq {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)

theorem Filter.EventuallyEq.tendsto {X : Type u} [TopologicalSpace X] {α : Type u_1} {x : X} {l : Filter α} {f : α → X} (hf : f =ᶠ[l] fun (x_1 : α) => x) : Tendsto f l (nhds x)

Interior, closure and frontier in terms of neighborhoods

theorem interior_eq_nhds' {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = {x : X | s ∈ nhds x}

theorem interior_eq_nhds {X : Type u} [TopologicalSpace X] {s : Set X} : interior s = {x : X | nhds x ≤ Filter.principal s}

@[simp]

theorem interior_mem_nhds {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : interior s ∈ nhds x ↔ s ∈ nhds x

theorem interior_setOf_eq {X : Type u} [TopologicalSpace X] {p : X → Prop} : interior {x : X | p x} = {x : X | ∀ᶠ (y : X) in nhds x, p y}

theorem isOpen_setOf_eventually_nhds {X : Type u} [TopologicalSpace X] {p : X → Prop} : IsOpen {x : X | ∀ᶠ (y : X) in nhds x, p y}

theorem subset_interior_iff_nhds {X : Type u} [TopologicalSpace X] {s V : Set X} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ nhds x

theorem isOpen_iff_nhds {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, nhds x ≤ Filter.principal s

theorem TopologicalSpace.ext_iff_nhds {X : Type u_2} {t t' : TopologicalSpace X} : t = t' ↔ ∀ (x : X), nhds x = nhds x

theorem TopologicalSpace.ext_nhds {X : Type u_2} {t t' : TopologicalSpace X} : (∀ (x : X), nhds x = nhds x) → t = t'

Alias of the reverse direction of TopologicalSpace.ext_iff_nhds.

theorem isOpen_iff_mem_nhds {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, s ∈ nhds x

theorem isOpen_iff_eventually {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, y ∈ s

A set s is open iff for every point x in s and every y close to x, y is in s.

theorem isOpen_singleton_iff_nhds_eq_pure {X : Type u} [TopologicalSpace X] (x : X) : IsOpen {x} ↔ nhds x = pure x

theorem isOpen_singleton_iff_punctured_nhds {X : Type u} [TopologicalSpace X] (x : X) : IsOpen {x} ↔ nhdsWithin x {x}ᶜ = ⊥

theorem mem_closure_iff_frequently {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : x ∈ closure s ↔ ∃ᶠ (x : X) in nhds x, x ∈ s

theorem Filter.Frequently.mem_closure {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : (∃ᶠ (x : X) in nhds x, x ∈ s) → x ∈ closure s

Alias of the reverse direction of mem_closure_iff_frequently.

theorem isClosed_iff_frequently {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in nhds x, y ∈ s) → x ∈ s

A set s is closed iff for every point x, if there is a point y close to x that belongs to s then x is in s.

theorem nhdsWithin_neBot {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} : (nhdsWithin x s).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ nhds x → (t ∩ s).Nonempty

theorem nhdsWithin_mono {X : Type u} [TopologicalSpace X] (x : X) {s t : Set X} (h : s ⊆ t) : nhdsWithin x s ≤ nhdsWithin x t

theorem IsClosed.interior_union_left {X : Type u} [TopologicalSpace X] {s t : Set X} : IsClosed s → interior (s ∪ t) ⊆ s ∪ interior t

theorem IsClosed.interior_union_right {X : Type u} [TopologicalSpace X] {s t : Set X} (h : IsClosed t) : interior (s ∪ t) ⊆ interior s ∪ t

theorem IsOpen.inter_closure {X : Type u} [TopologicalSpace X] {s t : Set X} (h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t)

theorem IsOpen.closure_inter {X : Type u} [TopologicalSpace X] {s t : Set X} (h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t)

theorem Dense.open_subset_closure_inter {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : IsOpen t) : t ⊆ closure (t ∩ s)

theorem Dense.inter_of_isOpen_left {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : Dense (s ∩ t)

The intersection of an open dense set with a dense set is a dense set.

theorem Dense.inter_of_isOpen_right {X : Type u} [TopologicalSpace X] {s t : Set X} (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : Dense (s ∩ t)

The intersection of a dense set with an open dense set is a dense set.

theorem Dense.inter_nhds_nonempty {X : Type u} [TopologicalSpace X] {x : X} {s t : Set X} (hs : Dense s) (ht : t ∈ nhds x) : (s ∩ t).Nonempty

theorem closure_diff {X : Type u} [TopologicalSpace X] {s t : Set X} : closure s \ closure t ⊆ closure (s \ t)

theorem Filter.Frequently.mem_of_closed {X : Type u} [TopologicalSpace X] {x : X} {s : Set X} (h : ∃ᶠ (x : X) in nhds x, x ∈ s) (hs : IsClosed s) : x ∈ s

theorem IsClosed.mem_of_frequently_of_tendsto {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

theorem IsClosed.mem_of_tendsto {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

theorem mem_closure_of_frequently_of_tendsto {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

theorem mem_closure_of_tendsto {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

theorem tendsto_inf_principal_nhds_iff_of_forall_eq {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)

Suppose that f sends the complement to s to a single point x, and l is some filter. Then f tends to x along l restricted to s if and only if it tends to x along l.