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 ∈ t → s ∈ 𝓝 x
usingmem_nhdsSet_iff_forall
∃ U : Set α, 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
.
The filter of neighborhoods of a set in a topological space.
Equations
- Topology.«term𝓝ˢ» = Lean.ParserDescr.node `Topology.term𝓝ˢ 1024 (Lean.ParserDescr.symbol "𝓝ˢ")
theorem
nhdsSet_diagonal
(α : Type u_1)
[inst : TopologicalSpace (α × α)]
:
nhdsSet (Set.diagonal α) = ⨆ x, nhds (x, x)
theorem
bUnion_mem_nhdsSet
{α : Type u_1}
[inst : TopologicalSpace α]
{s : Set α}
{t : α → Set α}
(h : ∀ (x : α), x ∈ s → t x ∈ nhds x)
:
(Set.unionᵢ fun x => Set.unionᵢ fun h => t x) ∈ nhdsSet s
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
hasBasis_nhdsSet
{α : Type u_1}
[inst : TopologicalSpace α]
(s : Set α)
:
Filter.HasBasis (nhdsSet s) (fun U => IsOpen U ∧ s ⊆ U) fun U => U
theorem
principal_le_nhdsSet
{α : Type u_1}
[inst : TopologicalSpace α]
{s : Set α}
:
Filter.principal s ≤ nhdsSet s
@[simp]
theorem
nhdsSet_eq_principal_iff
{α : Type u_1}
[inst : TopologicalSpace α]
{s : Set α}
:
nhdsSet s = Filter.principal s ↔ IsOpen s
theorem
IsOpen.nhdsSet_eq
{α : Type u_1}
[inst : TopologicalSpace α]
{s : Set α}
:
IsOpen s → nhdsSet s = Filter.principal s
Alias of the reverse direction of nhdsSet_eq_principal_iff
.
@[simp]
theorem
nhdsSet_interior
{α : Type u_1}
[inst : TopologicalSpace α]
{s : Set α}
:
nhdsSet (interior s) = Filter.principal (interior s)
@[simp]
@[simp]
theorem
nhds_le_nhdsSet
{α : Type u_1}
[inst : TopologicalSpace α]
{s : Set α}
{x : α}
(h : x ∈ s)
:
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)
:
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
.