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
usingsubset_interior_iff_mem_nhdsSet
β x : X, x β t β s β π x
usingmem_nhdsSet_iff_forall
β U : Set X, IsOpen U β§ t β U β§ U β s
usingmem_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 inMathlib.Topology.Separation
.
theorem
nhdsSet_diagonal
(X : Type u_3)
[TopologicalSpace (X Γ X)]
:
nhdsSet (Set.diagonal X) = β¨ (x : X), nhds (x, x)
theorem
bUnion_mem_nhdsSet
{X : Type u_1}
[TopologicalSpace X]
{s : Set X}
{t : X β Set X}
(h : β x β s, t x β nhds x)
:
theorem
eventually_nhdsSet_iff_forall
{X : Type u_1}
[TopologicalSpace X]
{s : Set X}
{p : X β Prop}
:
A proposition is true on a set neighborhood of s
iff it is eventually true near each point in the set.
@[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)
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
@[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
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
IsClosed.nhdsSet_le_sup
{X : Type u_1}
[TopologicalSpace X]
(s : Set X)
{t : Set X}
(h : IsClosed t)
:
theorem
IsClosed.nhdsSet_le_sup'
{X : Type u_1}
[TopologicalSpace X]
(s : Set X)
{t : Set X}
(h : IsClosed 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)
:
theorem
eventually_nhdsSet_iUnion
{X : Type u_1}
[TopologicalSpace X]
{ΞΉ : Sort u_3}
{s : ΞΉ β Set X}
{P : X β Prop}
: