# mathlib3documentation

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:

• s ⊆ interior t using subset_interior_iff_mem_nhds_set
• ∀ (x : α), x ∈ t → s ∈ 𝓝 x using mem_nhds_set_iff_forall
• ∃ U : set α, is_open U ∧ t ⊆ U ∧ U ⊆ s using mem_nhds_set_iff_exists

Furthermore, we have the following results:

• monotone_nhds_set: 𝓝ˢ is monotone
• In T₁-spaces, 𝓝ˢis strictly monotone and hence injective: strict_mono_nhds_set/injective_nhds_set. These results are in topology.separation.
def nhds_set {α : Type u_1} (s : set α) :

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

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

Alias of the reverse direction of nhds_set_eq_principal_iff.

@[simp]
theorem nhds_set_interior {α : Type u_1} {s : set α} :
@[simp]
theorem nhds_set_singleton {α : Type u_1} {x : α} :
theorem mem_nhds_set_interior {α : Type u_1} {s : set α} :
@[simp]
theorem nhds_set_empty {α : Type u_1}  :
theorem mem_nhds_set_empty {α : Type u_1} {s : set α} :
@[simp]
theorem nhds_set_univ {α : Type u_1}  :
theorem nhds_set_mono {α : Type u_1} {s t : set α} (h : s t) :
theorem monotone_nhds_set {α : Type u_1}  :
theorem nhds_le_nhds_set {α : Type u_1} {s : set α} {x : α} (h : x s) :
@[simp]
theorem nhds_set_union {α : Type u_1} (s t : set α) :
nhds_set (s t) =
theorem union_mem_nhds_set {α : Type u_1} {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} {s : set α} {f : α β} {t : set β} (hf : continuous f) (hst : 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.