mathlib3 documentation

topology.nhds_set

Neighborhoods of a set #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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

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

Equations
source
theorem nhds_set_diagonal (α : Type u_1) [topological_space (α × α)] :
nhds_set (set.diagonal α) = ⨆ (x : α), nhds (x, x)
source
theorem mem_nhds_set_iff_forall {α : Type u_1} [topological_space α] {s t : set α} :
s ∈ nhds_set t ↔ ∀ (x : α), x ∈ t → s ∈ nhds x
source
theorem bUnion_mem_nhds_set {α : Type u_1} [topological_space α] {s : set α} {t : α → set α} (h : ∀ (x : α), x ∈ s → t x ∈ nhds x) :
(⋃ (x : α) (H : x ∈ s), t x) ∈ nhds_set s
source
theorem subset_interior_iff_mem_nhds_set {α : Type u_1} [topological_space α] {s t : set α} :
s ⊆ interior t ↔ t ∈ nhds_set s
source
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
source
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)
source
theorem is_open.mem_nhds_set {α : Type u_1} [topological_space α] {s t : set α} (hU : is_open s) :
s ∈ nhds_set t ↔ t ⊆ s
source
theorem principal_le_nhds_set {α : Type u_1} [topological_space α] {s : set α} :
filter.principal s ≤ nhds_set s
source
@[simp]
theorem nhds_set_eq_principal_iff {α : Type u_1} [topological_space α] {s : set α} :
nhds_set s = filter.principal s ↔ is_open s
source
theorem is_open.nhds_set_eq {α : Type u_1} [topological_space α] {s : set α} :
is_open s → nhds_set s = filter.principal s

Alias of the reverse direction of nhds_set_eq_principal_iff.

source
@[simp]
theorem nhds_set_interior {α : Type u_1} [topological_space α] {s : set α} :
nhds_set (interior s) = filter.principal (interior s)
source
@[simp]
theorem nhds_set_singleton {α : Type u_1} [topological_space α] {x : α} :
nhds_set {x} = nhds x
source
theorem mem_nhds_set_interior {α : Type u_1} [topological_space α] {s : set α} :
s ∈ nhds_set (interior s)
source
@[simp]
theorem nhds_set_empty {α : Type u_1} [topological_space α] :
nhds_set ∅ = ⊥
source
theorem mem_nhds_set_empty {α : Type u_1} [topological_space α] {s : set α} :
s ∈ nhds_set ∅
source
@[simp]
theorem nhds_set_univ {α : Type u_1} [topological_space α] :
nhds_set set.univ = ⊤
source
theorem nhds_set_mono {α : Type u_1} [topological_space α] {s t : set α} (h : s ⊆ t) :
nhds_set s ≤ nhds_set t
source
theorem monotone_nhds_set {α : Type u_1} [topological_space α] :
monotone nhds_set
source
theorem nhds_le_nhds_set {α : Type u_1} [topological_space α] {s : set α} {x : α} (h : x ∈ s) :
nhds x ≤ nhds_set s
source
@[simp]
theorem nhds_set_union {α : Type u_1} [topological_space α] (s t : set α) :
nhds_set (s ∪ t) = nhds_set s ⊔ nhds_set t
source
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₂)
source
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) :
filter.tendsto f (nhds_set s) (nhds_set 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.