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:

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 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) :
Filter.HasBasis (nhdsSet s) (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) :
Filter.lift' (nhdsSet s) 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 : Filter.HasBasis (nhdsSet t) p s) :
Filter.HasBasis (nhdsSet t) 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) :
theorem IsOpen.mem_nhdsSet_self {X : Type u_1} [TopologicalSpace X] {s : Set X} (ho : IsOpen s) :

An open set belongs to its own set neighborhoods filter.

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} {Y : Type u_2} [TopologicalSpace X] {s : Set X} {f : X β†’ Y} {g : X β†’ Y} (h : f =αΆ [nhdsSet s] g) :
Set.EqOn f g s
theorem IsOpen.nhdsSet_eq {X : Type u_1} [TopologicalSpace X] {s : Set X} :

Alias of the reverse direction of nhdsSet_eq_principal_iff.

@[simp]
theorem nhdsSet_singleton {X : Type u_1} [TopologicalSpace X] {x : X} :
nhdsSet {x} = nhds x
@[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) :
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) :
@[simp]
theorem nhdsSet_union {X : Type u_1} [TopologicalSpace X] (s : Set X) (t : Set X) :
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) :
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) :

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) :
theorem nhdsSet_inter_le {X : Type u_1} [TopologicalSpace X] (s : Set X) (t : Set X) :
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