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:

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} [topological_space α] (s : set α) :

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

Equations

𝓝ˢ s = Sup (𝓝 '' s)

theorem mem_nhds_set_iff_forall {α : Type u_1} [topological_space α] {s t : set α} :

s ∈ 𝓝ˢ t ↔ ∀ (x : α), x ∈ t → s ∈ 𝓝 x

theorem subset_interior_iff_mem_nhds_set {α : Type u_1} [topological_space α] {s t : set α} :

s ⊆ interior t ↔ t ∈ 𝓝ˢ s

theorem mem_nhds_set_iff_exists {α : Type u_1} [topological_space α] {s t : set α} :

s ∈ 𝓝ˢ t ↔ ∃ (U : set α), is_open U ∧ t ⊆ U ∧ U ⊆ s

theorem has_basis_nhds_set {α : Type u_1} [topological_space α] (s : 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) :

s ∈ 𝓝ˢ t ↔ t ⊆ s

@[simp]

theorem nhds_set_singleton {α : Type u_1} [topological_space α] {x : α} :

𝓝ˢ {x} = 𝓝 x

theorem mem_nhds_set_interior {α : Type u_1} [topological_space α] {s : set α} :

s ∈ 𝓝ˢ (interior s)

theorem mem_nhds_set_empty {α : Type u_1} [topological_space α] {s : set α} :

s ∈ 𝓝ˢ ∅

@[simp]

theorem nhds_set_empty {α : Type u_1} [topological_space α] :

𝓝ˢ ∅ = ⊥

@[simp]

theorem nhds_set_univ {α : Type u_1} [topological_space α] :

𝓝ˢ set.univ = ⊤

theorem monotone_nhds_set {α : Type u_1} [topological_space α] :

monotone 𝓝ˢ

@[simp]

theorem nhds_set_union {α : Type u_1} [topological_space α] (s t : set α) :

𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t

theorem union_mem_nhds_set {α : Type u_1} [topological_space α] {s₁ s₂ t₁ t₂ : set α} (h₁ : s₁ ∈ 𝓝ˢ t₁) (h₂ : s₂ ∈ 𝓝ˢ t₂) :

s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)