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)] :
= β¨ (x : X), nhds (x, x)
theorem mem_nhdsSet_iff_forall {X : Type u_1} [] {s : Set X} {t : Set X} :
s β β β x β t, s β nhds x
theorem nhdsSet_le {X : Type u_1} [] {f : } {s : Set X} :
β€ f β β x β s, nhds x β€ f
theorem bUnion_mem_nhdsSet {X : Type u_1} [] {s : Set X} {t : X β Set X} (h : β x β s, t x β nhds x) :
β x β s, t x β
theorem subset_interior_iff_mem_nhdsSet {X : Type u_1} [] {s : Set X} {t : Set X} :
theorem disjoint_principal_nhdsSet {X : Type u_1} [] {s : Set X} {t : Set X} :
theorem disjoint_nhdsSet_principal {X : Type u_1} [] {s : Set X} {t : Set X} :
theorem mem_nhdsSet_iff_exists {X : Type u_1} [] {s : Set X} {t : Set X} :
s β β β (U : Set X), β§ t β U β§ U β s
theorem eventually_nhdsSet_iff_exists {X : Type u_1} [] {s : Set X} {p : X β Prop} :
(βαΆ  (x : X) in , p x) β β (t : Set X), β§ 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} [] {s : Set X} {p : X β Prop} :
(βαΆ  (x : X) in , 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} [] (s : Set X) :
().HasBasis (fun (U : Set X) => β§ s β U) fun (U : Set X) => U
@[simp]
theorem lift'_nhdsSet_interior {X : Type u_1} [] (s : Set X) :
().lift' interior =
theorem Filter.HasBasis.nhdsSet_interior {X : Type u_1} [] {ΞΉ : Sort u_3} {p : ΞΉ β Prop} {s : ΞΉ β Set X} {t : Set X} (h : ().HasBasis p s) :
().HasBasis p fun (x : ΞΉ) => interior (s x)
theorem IsOpen.mem_nhdsSet {X : Type u_1} [] {s : Set X} {t : Set X} (hU : ) :
theorem IsOpen.mem_nhdsSet_self {X : Type u_1} [] {s : Set X} (ho : ) :

An open set belongs to its own set neighborhoods filter.

theorem principal_le_nhdsSet {X : Type u_1} [] {s : Set X} :
theorem subset_of_mem_nhdsSet {X : Type u_1} [] {s : Set X} {t : Set X} (h : t β ) :
s β t
theorem Filter.Eventually.self_of_nhdsSet {X : Type u_1} [] {s : Set X} {p : X β Prop} (h : βαΆ  (x : X) in , p x) (x : X) :
x β s β p x
theorem Filter.EventuallyEq.self_of_nhdsSet {X : Type u_1} {Y : Type u_2} [] {s : Set X} {f : X β Y} {g : X β Y} (h : f =αΆ [] g) :
Set.EqOn f g s
@[simp]
theorem nhdsSet_eq_principal_iff {X : Type u_1} [] {s : Set X} :
theorem IsOpen.nhdsSet_eq {X : Type u_1} [] {s : Set X} :
β

Alias of the reverse direction of nhdsSet_eq_principal_iff.

@[simp]
theorem nhdsSet_interior {X : Type u_1} [] {s : Set X} :
@[simp]
theorem nhdsSet_singleton {X : Type u_1} [] {x : X} :
nhdsSet {x} = nhds x
theorem mem_nhdsSet_interior {X : Type u_1} [] {s : Set X} :
@[simp]
theorem nhdsSet_empty {X : Type u_1} [] :
theorem mem_nhdsSet_empty {X : Type u_1} [] {s : Set X} :
@[simp]
theorem nhdsSet_univ {X : Type u_1} [] :
nhdsSet Set.univ = β€
theorem nhdsSet_mono {X : Type u_1} [] {s : Set X} {t : Set X} (h : s β t) :
theorem monotone_nhdsSet {X : Type u_1} [] :
Monotone nhdsSet
theorem nhds_le_nhdsSet {X : Type u_1} [] {s : Set X} {x : X} (h : x β s) :
@[simp]
theorem nhdsSet_union {X : Type u_1} [] (s : Set X) (t : Set X) :
theorem union_mem_nhdsSet {X : Type u_1} [] {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} [] (x : X) (s : Set X) :
theorem Continuous.tendsto_nhdsSet {X : Type u_1} {Y : Type u_2} [] [] {s : Set X} {f : X β Y} {t : Set Y} (hf : ) (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} [] [] {s : Set X} {y : Y} {f : X β Y} (h : ) (h' : Set.EqOn f (fun (x : X) => y) s) :
theorem nhdsSet_inter_le {X : Type u_1} [] (s : Set X) (t : Set X) :
theorem IsClosed.nhdsSet_le_sup {X : Type u_1} [] (s : Set X) {t : Set X} (h : ) :
theorem IsClosed.nhdsSet_le_sup' {X : Type u_1} [] (s : Set X) {t : Set X} (h : ) :
theorem Filter.Eventually.eventually_nhdsSet {X : Type u_1} [] {s : Set X} {p : X β Prop} (h : βαΆ  (y : X) in , p y) :
βαΆ  (y : X) in , βαΆ  (x : X) in nhds y, p x
theorem Filter.Eventually.union_nhdsSet {X : Type u_1} [] {s : Set X} {t : Set X} {p : X β Prop} :
(βαΆ  (x : X) in nhdsSet (s βͺ t), p x) β (βαΆ  (x : X) in , p x) β§ βαΆ  (x : X) in , p x
theorem Filter.Eventually.union {X : Type u_1} [] {s : Set X} {t : Set X} {p : X β Prop} (hs : βαΆ  (x : X) in , p x) (ht : βαΆ  (x : X) in , p x) :
βαΆ  (x : X) in nhdsSet (s βͺ t), p x
theorem nhdsSet_iUnion {X : Type u_1} [] {ΞΉ : Sort u_3} (s : ΞΉ β Set X) :
nhdsSet (β (i : ΞΉ), s i) = β¨ (i : ΞΉ), nhdsSet (s i)
theorem eventually_nhdsSet_iUnionβ {X : Type u_1} [] {ΞΉ : 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} [] {ΞΉ : 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