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:

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

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

Equations
theorem nhds_set_diagonal (α : Type u_1) [topological_space × α)] :
nhds_set (set.diagonal α) = (x : α), nhds (x, x)
theorem mem_nhds_set_iff_forall {α : Type u_1} [topological_space α] {s t : set α} :
s nhds_set t (x : α), x t s nhds x
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
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) :
@[simp]
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]
@[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_mono {α : Type u_1} [topological_space α] {s t : set α} (h : s t) :
theorem nhds_le_nhds_set {α : Type u_1} [topological_space α] {s : set α} {x : α} (h : x s) :
@[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.