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, x ∈ t → s ∈ 𝓝 x using mem_nhdsSet_iff_forall
• ∃ U : Set X, 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.

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

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

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

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

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

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

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

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

theorem eventually_nhdsSet_iff_exists {X : Type u_1} [TopologicalSpace X] {s : Set X} {p : X → Prop} : (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∃ (t : Set X), 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 {X : Type u_1} [TopologicalSpace X] {s : Set X} {p : X → Prop} : (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∀ x ∈ s, ∀ᶠ (y : X) 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 {X : Type u_1} [TopologicalSpace X] (s : Set X) : (nhdsSet s).HasBasis (fun (U : Set X) => IsOpen U ∧ s ⊆ U) fun (U : Set X) => U

@[simp]

theorem lift'_nhdsSet_interior {X : Type u_1} [TopologicalSpace X] (s : Set X) : (nhdsSet s).lift' interior = nhdsSet s

theorem Filter.HasBasis.nhdsSet_interior {X : Type u_1} [TopologicalSpace X] {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {t : Set X} (h : (nhdsSet t).HasBasis p s) : (nhdsSet t).HasBasis p fun (x : ι) => interior (s x)

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

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

An open set belongs to its own set neighborhoods filter.

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

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

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

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

@[simp]

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

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

Alias of the reverse direction of nhdsSet_eq_principal_iff.

@[simp]

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

theorem Continuous.tendsto_nhdsSet {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} {t : Set Y} (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_1} {Y : Type u_2} [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)

theorem nhdsSet_inter_le {X : Type u_1} [TopologicalSpace X] (s : Set X) (t : Set X) : nhdsSet (s ∩ t) ≤ nhdsSet s ⊓ nhdsSet t

theorem nhdsSet_iInter_le {X : Type u_1} [TopologicalSpace X] {ι : Sort u_3} (s : ι → Set X) : nhdsSet (⋂ (i : ι), s i) ≤ ⨅ (i : ι), nhdsSet (s i)

theorem nhdsSet_sInter_le {X : Type u_1} [TopologicalSpace X] (s : Set (Set X)) : nhdsSet (⋂₀ s) ≤ ⨅ x ∈ s, nhdsSet x

theorem IsClosed.nhdsSet_le_sup {X : Type u_1} [TopologicalSpace X] (s : Set X) {t : Set X} (h : IsClosed t) : nhdsSet s ≤ nhdsSet (s ∩ t) ⊔ Filter.principal tᶜ

theorem IsClosed.nhdsSet_le_sup' {X : Type u_1} [TopologicalSpace X] (s : Set X) {t : Set X} (h : IsClosed t) : nhdsSet s ≤ nhdsSet (t ∩ s) ⊔ Filter.principal tᶜ

theorem Filter.Eventually.eventually_nhdsSet {X : Type u_1} [TopologicalSpace X] {s : Set X} {p : X → Prop} (h : ∀ᶠ (y : X) in nhdsSet s, p y) : ∀ᶠ (y : X) in nhdsSet s, ∀ᶠ (x : X) in nhds y, p x

theorem Filter.Eventually.union_nhdsSet {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} {p : X → Prop} : (∀ᶠ (x : X) in nhdsSet (s ∪ t), p x) ↔ (∀ᶠ (x : X) in nhdsSet s, p x) ∧ ∀ᶠ (x : X) in nhdsSet t, p x

theorem Filter.Eventually.union {X : Type u_1} [TopologicalSpace X] {s : Set X} {t : Set X} {p : X → Prop} (hs : ∀ᶠ (x : X) in nhdsSet s, p x) (ht : ∀ᶠ (x : X) in nhdsSet t, p x) : ∀ᶠ (x : X) in nhdsSet (s ∪ t), p x

theorem nhdsSet_iUnion {X : Type u_1} [TopologicalSpace X] {ι : Sort u_3} (s : ι → Set X) : nhdsSet (⋃ (i : ι), s i) = ⨆ (i : ι), nhdsSet (s i)

theorem eventually_nhdsSet_iUnion₂ {X : Type u_1} [TopologicalSpace X] {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {P : X → Prop} : (∀ᶠ (x : X) in nhdsSet (⋃ (i : ι), ⋃ (_ : p i), s i), P x) ↔ ∀ (i : ι), p i → ∀ᶠ (x : X) in nhdsSet (s i), P x

theorem eventually_nhdsSet_iUnion {X : Type u_1} [TopologicalSpace X] {ι : Sort u_3} {s : ι → Set X} {P : X → Prop} : (∀ᶠ (x : X) in nhdsSet (⋃ (i : ι), s i), P x) ↔ ∀ (i : ι), ∀ᶠ (x : X) in nhdsSet (s i), P x