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.

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

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

Equations

• nhdsSet s = sSup (nhds '' s)

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 "𝓝ˢ")

theorem nhdsSet_diagonal (α : Type u_3) [TopologicalSpace (α × α)] : nhdsSet (Set.diagonal α) = ⨆ (x : α), nhds (x, x)

theorem mem_nhdsSet_iff_forall {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} : s ∈ nhdsSet t ↔ ∀ x ∈ t, s ∈ nhds x

theorem nhdsSet_le {α : Type u_1} [TopologicalSpace α] {f : Filter α} {s : Set α} : nhdsSet s ≤ f ↔ ∀ a ∈ s, nhds a ≤ f

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

theorem subset_interior_iff_mem_nhdsSet {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} : s ⊆ interior t ↔ t ∈ nhdsSet s

theorem disjoint_principal_nhdsSet {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} : Disjoint (Filter.principal s) (nhdsSet t) ↔ Disjoint (closure s) t

theorem disjoint_nhdsSet_principal {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} : Disjoint (nhdsSet s) (Filter.principal t) ↔ Disjoint s (closure t)

theorem mem_nhdsSet_iff_exists {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} : s ∈ nhdsSet t ↔ ∃ (U : Set α), IsOpen U ∧ t ⊆ U ∧ U ⊆ s

theorem eventually_nhdsSet_iff_exists {α : Type u_1} [TopologicalSpace α] {s : Set α} {p : α → Prop} : (∀ᶠ (x : α) in nhdsSet s, p x) ↔ ∃ (t : Set α), IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, p x

A proposition is true on a set neighborhood of s iff it is true on a larger open set

theorem eventually_nhdsSet_iff_forall {α : Type u_1} [TopologicalSpace α] {s : Set α} {p : α → Prop} : (∀ᶠ (x : α) in nhdsSet s, p x) ↔ ∀ x ∈ s, ∀ᶠ (y : α) in nhds x, p y

A proposition is true on a set neighborhood of s iff it is eventually true near each point in the set.

theorem hasBasis_nhdsSet {α : Type u_1} [TopologicalSpace α] (s : Set α) : Filter.HasBasis (nhdsSet s) (fun (U : Set α) => IsOpen U ∧ s ⊆ U) fun (U : Set α) => U

theorem IsOpen.mem_nhdsSet {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} (hU : IsOpen s) : s ∈ nhdsSet t ↔ t ⊆ s

theorem IsOpen.mem_nhdsSet_self {α : Type u_1} [TopologicalSpace α] {s : Set α} (ho : IsOpen s) : s ∈ nhdsSet s

An open set belongs to its own set neighborhoods filter.

theorem principal_le_nhdsSet {α : Type u_1} [TopologicalSpace α] {s : Set α} : Filter.principal s ≤ nhdsSet s

theorem subset_of_mem_nhdsSet {α : Type u_1} [TopologicalSpace α] {s : Set α} {t : Set α} (h : t ∈ nhdsSet s) : s ⊆ t

theorem Filter.Eventually.self_of_nhdsSet {α : Type u_1} [TopologicalSpace α] {s : Set α} {p : α → Prop} (h : ∀ᶠ (x : α) in nhdsSet s, p x) (x : α) : x ∈ s → p x

theorem Filter.EventuallyEq.self_of_nhdsSet {α : Type u_1} {β : Type u_2} [TopologicalSpace α] {s : Set α} {f : α → β} {g : α → β} (h : f =ᶠ[nhdsSet s] g) : Set.EqOn f g s

@[simp]

theorem nhdsSet_eq_principal_iff {α : Type u_1} [TopologicalSpace α] {s : Set α} : nhdsSet s = Filter.principal s ↔ IsOpen s

theorem IsOpen.nhdsSet_eq {α : Type u_1} [TopologicalSpace α] {s : Set α} : IsOpen s → nhdsSet s = Filter.principal s

Alias of the reverse direction of nhdsSet_eq_principal_iff.

@[simp]

theorem nhdsSet_interior {α : Type u_1} [TopologicalSpace α] {s : Set α} : nhdsSet (interior s) = Filter.principal (interior s)

@[simp]

theorem nhdsSet_singleton {α : Type u_1} [TopologicalSpace α] {x : α} : nhdsSet {x} = nhds x

theorem mem_nhdsSet_interior {α : Type u_1} [TopologicalSpace α] {s : Set α} : s ∈ nhdsSet (interior s)

@[simp]

theorem nhdsSet_empty {α : Type u_1} [TopologicalSpace α] : nhdsSet ∅ = ⊥

theorem mem_nhdsSet_empty {α : Type u_1} [TopologicalSpace α] {s : Set α} : s ∈ nhdsSet ∅

@[simp]

theorem nhdsSet_univ {α : Type u_1} [TopologicalSpace α] : nhdsSet Set.univ = ⊤

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

theorem monotone_nhdsSet {α : Type u_1} [TopologicalSpace α] : Monotone nhdsSet

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

@[simp]

theorem nhdsSet_union {α : Type u_1} [TopologicalSpace α] (s : Set α) (t : Set α) : nhdsSet (s ∪ t) = nhdsSet s ⊔ nhdsSet t

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

@[simp]

theorem nhdsSet_insert {α : Type u_1} [TopologicalSpace α] (x : α) (s : Set α) : nhdsSet (insert x s) = nhds x ⊔ nhdsSet s

theorem Continuous.tendsto_nhdsSet {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [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.

theorem Continuous.tendsto_nhdsSet_nhds {X : Type u_3} {Y : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {y : Y} {f : X → Y} (h : Continuous f) (h' : Set.EqOn f (fun (x : X) => y) s) : Filter.Tendsto f (nhdsSet s) (nhds y)