Documentation

Mathlib.Topology.NhdsSet

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:

Furthermore, we have the following results:

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

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

Equations

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

Equations
theorem nhdsSet_diagonal (α : Type u_1) [inst : TopologicalSpace (α × α)] :
nhdsSet (Set.diagonal α) = x, nhds (x, x)
theorem mem_nhdsSet_iff_forall {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :
s nhdsSet t ∀ (x : α), x ts nhds x
theorem bUnion_mem_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : αSet α} (h : ∀ (x : α), x st x nhds x) :
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) nhdsSet s
theorem subset_interior_iff_mem_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :
theorem disjoint_principal_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :
theorem disjoint_nhdsSet_principal {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :
theorem mem_nhdsSet_iff_exists {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :
s nhdsSet t U, IsOpen U t U U s
theorem hasBasis_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) :
Filter.HasBasis (nhdsSet s) (fun U => IsOpen U s U) fun U => U
theorem IsOpen.mem_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (hU : IsOpen s) :
s nhdsSet t t s
@[simp]
theorem nhdsSet_eq_principal_iff {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :
theorem IsOpen.nhdsSet_eq {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :

Alias of the reverse direction of nhdsSet_eq_principal_iff.

@[simp]
theorem nhdsSet_interior {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :
@[simp]
theorem nhdsSet_singleton {α : Type u_1} [inst : TopologicalSpace α] {x : α} :
nhdsSet {x} = nhds x
theorem mem_nhdsSet_interior {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :
@[simp]
theorem nhdsSet_empty {α : Type u_1} [inst : TopologicalSpace α] :
theorem mem_nhdsSet_empty {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} :
@[simp]
theorem nhdsSet_univ {α : Type u_1} [inst : TopologicalSpace α] :
nhdsSet Set.univ =
theorem nhdsSet_mono {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (h : s t) :
theorem monotone_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] :
Monotone nhdsSet
theorem nhds_le_nhdsSet {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} (h : x s) :
@[simp]
theorem nhdsSet_union {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) (t : Set α) :
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₂)
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) :

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.