Neighborhoods of a set #

In this file we define the filter 𝓝ˢ s or nhdsSet 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_nhdsSet
∀ x : α, x ∈ t → s ∈ 𝓝 x using mem_nhdsSet_iff_forall
∃ U : Set α, IsOpen U ∧ t ⊆ U ∧ U ⊆ s using mem_nhdsSet_iff_exists

Furthermore, we have the following results:

monotone_nhdsSet: 𝓝ˢ is monotone
In T₁-spaces, 𝓝ˢis strictly monotone and hence injective: strict_mono_nhdsSet/injective_nhdsSet. These results are in Mathlib.Topology.Separation.

source

ink

def nhdsSet {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) :

Filter α

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

Equations

nhdsSet s = supₛ (nhds '' s)

source

ink

def Topology.«term𝓝ˢ» :

Lean.ParserDescr

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

Equations

Topology.«term𝓝ˢ» = Lean.ParserDescr.node `Topology.term𝓝ˢ 1024 (Lean.ParserDescr.symbol "𝓝ˢ")

source

ink

theorem nhdsSet_diagonal (α : Type u_1) [inst : TopologicalSpace (α × α)] :

nhdsSet (Set.diagonal α) = ⨆ x, nhds (x, x)

source

ink

theorem mem_nhdsSet_iff_forall {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

s ∈ nhdsSet t ↔ ∀ (x : α), x ∈ t → s ∈ nhds x

source

ink

theorem bUnion_mem_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : α → Set α} (h : ∀ (x : α), x ∈ s → t x ∈ nhds x) :

(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) ∈ nhdsSet s

source

ink

theorem subset_interior_iff_mem_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

s ⊆ interior t ↔ t ∈ nhdsSet s

source

ink

theorem disjoint_principal_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

Disjoint (Filter.principal s) (nhdsSet t) ↔ Disjoint (closure s) t

source

ink

theorem disjoint_nhdsSet_principal {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

Disjoint (nhdsSet s) (Filter.principal t) ↔ Disjoint s (closure t)

source

ink

theorem mem_nhdsSet_iff_exists {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

s ∈ nhdsSet t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s

source

ink

theorem hasBasis_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) :

Filter.HasBasis (nhdsSet s) (fun U => IsOpen U ∧ s ⊆ U) fun U => U

source

ink

theorem IsOpen.mem_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (hU : IsOpen s) :

s ∈ nhdsSet t ↔ t ⊆ s

source

ink

theorem principal_le_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :

Filter.principal s ≤ nhdsSet s

source

ink

@[simp]

theorem nhdsSet_eq_principal_iff {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :

nhdsSet s = Filter.principal s ↔ IsOpen s

source

ink

theorem IsOpen.nhdsSet_eq {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :

IsOpen s → nhdsSet s = Filter.principal s

Alias of the reverse direction of nhdsSet_eq_principal_iff.

source

ink

@[simp]

theorem nhdsSet_interior {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :

nhdsSet (interior s) = Filter.principal (interior s)

source

ink

@[simp]

theorem nhdsSet_singleton {α : Type u_1} [inst : TopologicalSpace α] {x : α} :

nhdsSet {x} = nhds x

source

ink

theorem mem_nhdsSet_interior {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :

s ∈ nhdsSet (interior s)

source

ink

@[simp]

theorem nhdsSet_empty {α : Type u_1} [inst : TopologicalSpace α] :

nhdsSet ∅ = ⊥

source

ink

theorem mem_nhdsSet_empty {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :

s ∈ nhdsSet ∅

source

ink

@[simp]

theorem nhdsSet_univ {α : Type u_1} [inst : TopologicalSpace α] :

nhdsSet Set.univ = ⊤

source

ink

theorem nhdsSet_mono {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (h : s ⊆ t) :

nhdsSet s ≤ nhdsSet t

source

ink

theorem monotone_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] :

Monotone nhdsSet

source

ink

theorem nhds_le_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} (h : x ∈ s) :

nhds x ≤ nhdsSet s

source

ink

@[simp]

theorem nhdsSet_union {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) (t : Set α) :

nhdsSet (s ∪ t) = nhdsSet s ⊔ nhdsSet t

source

ink

theorem union_mem_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s₁ : Set α} {s₂ : Set α} {t₁ : Set α} {t₂ : Set α} (h₁ : s₁ ∈ nhdsSet t₁) (h₂ : s₂ ∈ nhdsSet t₂) :

s₁ ∪ s₂ ∈ nhdsSet (t₁ ∪ t₂)

source

ink

theorem Continuous.tendsto_nhdsSet {α : Type u_2} {β : Type u_1} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {s : Set α} {f : α → β} {t : Set β} (hf : Continuous f) (hst : Set.MapsTo f s t) :

Filter.Tendsto f (nhdsSet s) (nhdsSet 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.