mathlib documentation

topology.nhds_set

Neighborhoods of a set #

In this file we define the filter 𝓝ˢ s or nhds_set s consisting of all neighborhoods of a set s.

Main Properties #

There are a couple different notions equivalent to s ∈ 𝓝ˢ t:

Furthermore, we have the following results:

def nhds_set {α : Type u_1} [topological_space α] (s : set α) :

The filter of neighborhoods of a set in a topological space.

Equations
theorem mem_nhds_set_iff_forall {α : Type u_1} [topological_space α] {s t : set α} :
s nhds_set t ∀ (x : α), x ts nhds x
theorem subset_interior_iff_mem_nhds_set {α : Type u_1} [topological_space α] {s t : set α} :
theorem mem_nhds_set_iff_exists {α : Type u_1} [topological_space α] {s t : set α} :
s nhds_set t ∃ (U : set α), is_open U t U U s
theorem has_basis_nhds_set {α : Type u_1} [topological_space α] (s : set α) :
(nhds_set s).has_basis (λ (U : set α), is_open U s U) (λ (U : set α), U)
theorem is_open.mem_nhds_set {α : Type u_1} [topological_space α] {s t : set α} (hU : is_open s) :
theorem principal_le_nhds_set {α : Type u_1} [topological_space α] {s : set α} :
@[simp]
theorem nhds_set_eq_principal_iff {α : Type u_1} [topological_space α] {s : set α} :
theorem is_open.nhds_set_eq {α : Type u_1} [topological_space α] {s : set α} :

Alias of the reverse direction of nhds_set_eq_principal_iff.

@[simp]
theorem nhds_set_interior {α : Type u_1} [topological_space α] {s : set α} :
@[simp]
theorem nhds_set_singleton {α : Type u_1} [topological_space α] {x : α} :
theorem mem_nhds_set_interior {α : Type u_1} [topological_space α] {s : set α} :
@[simp]
theorem nhds_set_empty {α : Type u_1} [topological_space α] :
theorem mem_nhds_set_empty {α : Type u_1} [topological_space α] {s : set α} :
@[simp]
theorem nhds_set_univ {α : Type u_1} [topological_space α] :
theorem monotone_nhds_set {α : Type u_1} [topological_space α] :
@[simp]
theorem nhds_set_union {α : Type u_1} [topological_space α] (s t : set α) :
theorem union_mem_nhds_set {α : Type u_1} [topological_space α] {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ nhds_set t₁) (h₂ : s₂ nhds_set t₂) :
s₁ s₂ nhds_set (t₁ t₂)
theorem continuous.tendsto_nhds_set {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {f : α → β} {t : set β} (hf : continuous f) (hst : set.maps_to f s t) :

Preimage of a set neighborhood of t under a continuous map f is a set neighborhood of s provided that f maps s to t.