# Topology on the set of filters on a type #

This file introduces a topology on Filter α. It is generated by the sets Set.Iic (𝓟 s) = {l : Filter α | s ∈ l}, s : Set α. A set s : Set (Filter α) is open if and only if it is a union of a family of these basic open sets, see Filter.isOpen_iff.

This topology has the following important properties.

• If X is a topological space, then the map 𝓝 : X → Filter X is a topology inducing map.

• In particular, it is a continuous map, so 𝓝 ∘ f tends to 𝓝 (𝓝 a) whenever f tends to 𝓝 a.

• If X is an ordered topological space with order topology and no max element, then 𝓝 ∘ f tends to 𝓝 Filter.atTop whenever f tends to Filter.atTop.

• It turns Filter X into a T₀ space and the order on Filter X is the dual of the specializationOrder (Filter X).

## Tags #

filter, topological space

The topology on Filter α is generated by the sets Set.Iic (𝓟 s) = {l : Filter α | s ∈ l}, s : Set α. A set s : Set (Filter α) is open if and only if it is a union of a family of these basic open sets, see Filter.isOpen_iff.

Equations
theorem Filter.isOpen_Iic_principal {α : Type u_2} {s : Set α} :
theorem Filter.isOpen_setOf_mem {α : Type u_2} {s : Set α} :
IsOpen {l : | s l}
theorem Filter.isOpen_iff {α : Type u_2} {s : Set ()} :
∃ (T : Set (Set α)), s = ⋃ t ∈ T,
theorem Filter.nhds_eq {α : Type u_2} (l : ) :
nhds l = Filter.lift' l (Set.Iic Filter.principal)
theorem Filter.nhds_eq' {α : Type u_2} (l : ) :
nhds l = Filter.lift' l fun (s : Set α) => {l' : | s l'}
theorem Filter.tendsto_nhds {α : Type u_2} {β : Type u_3} {la : } {lb : } {f : α} :
Filter.Tendsto f la (nhds lb) slb, ∀ᶠ (a : α) in la, s f a
theorem Filter.HasBasis.nhds {ι : Sort u_1} {α : Type u_2} {l : } {p : ιProp} {s : ιSet α} (h : ) :
Filter.HasBasis (nhds l) p fun (i : ι) => Set.Iic (Filter.principal (s i))
theorem Filter.tendsto_pure_self {X : Type u_4} (l : ) :
Filter.Tendsto pure l (nhds l)
instance Filter.instIsCountablyGeneratedFilterNhds {α : Type u_2} {l : } :

Neighborhoods of a countably generated filter is a countably generated filter.

Equations
• =
theorem Filter.HasBasis.nhds' {ι : Sort u_1} {α : Type u_2} {l : } {p : ιProp} {s : ιSet α} (h : ) :
Filter.HasBasis (nhds l) p fun (i : ι) => {l' : | s i l'}
theorem Filter.mem_nhds_iff {α : Type u_2} {l : } {S : Set ()} :
S nhds l ∃ t ∈ l, S
theorem Filter.mem_nhds_iff' {α : Type u_2} {l : } {S : Set ()} :
S nhds l ∃ t ∈ l, ∀ ⦃l' : ⦄, t l'l' S
@[simp]
theorem Filter.nhds_bot {α : Type u_2} :
@[simp]
theorem Filter.nhds_top {α : Type u_2} :
@[simp]
theorem Filter.nhds_principal {α : Type u_2} (s : Set α) :
@[simp]
theorem Filter.nhds_pure {α : Type u_2} (x : α) :
@[simp]
theorem Filter.nhds_iInf {ι : Sort u_1} {α : Type u_2} (f : ι) :
nhds (⨅ (i : ι), f i) = ⨅ (i : ι), nhds (f i)
@[simp]
theorem Filter.nhds_inf {α : Type u_2} (l₁ : ) (l₂ : ) :
nhds (l₁ l₂) = nhds l₁ nhds l₂
theorem Filter.monotone_nhds {α : Type u_2} :
theorem Filter.sInter_nhds {α : Type u_2} (l : ) :
⋂₀ {s : Set () | s nhds l} =
@[simp]
theorem Filter.nhds_mono {α : Type u_2} {l₁ : } {l₂ : } :
nhds l₁ nhds l₂ l₁ l₂
theorem Filter.mem_interior {α : Type u_2} {s : Set ()} {l : } :
l ∃ t ∈ l, s
theorem Filter.mem_closure {α : Type u_2} {s : Set ()} {l : } :
l tl, ∃ l' ∈ s, t l'
@[simp]
theorem Filter.closure_singleton {α : Type u_2} (l : ) :
closure {l} =
@[simp]
theorem Filter.specializes_iff_le {α : Type u_2} {l₁ : } {l₂ : } :
l₁ l₂ l₁ l₂
theorem Filter.nhds_atTop {α : Type u_2} [] :
nhds Filter.atTop = ⨅ (x : α),
theorem Filter.tendsto_nhds_atTop_iff {α : Type u_2} {β : Type u_3} [] {l : } {f : α} :
Filter.Tendsto f l (nhds Filter.atTop) ∀ (y : β), ∀ᶠ (a : α) in l, f a
theorem Filter.nhds_atBot {α : Type u_2} [] :
nhds Filter.atBot = ⨅ (x : α),
theorem Filter.tendsto_nhds_atBot_iff {α : Type u_2} {β : Type u_3} [] {l : } {f : α} :
Filter.Tendsto f l (nhds Filter.atBot) ∀ (y : β), ∀ᶠ (a : α) in l, f a
theorem Filter.nhds_nhds {X : Type u_4} [] (x : X) :
nhds (nhds x) = ⨅ (s : Set X), ⨅ (_ : ), ⨅ (_ : x s),
theorem Filter.inducing_nhds {X : Type u_4} [] :
theorem Filter.continuous_nhds {X : Type u_4} [] :
theorem Filter.Tendsto.nhds {α : Type u_2} {X : Type u_4} [] {f : αX} {l : } {x : X} (h : Filter.Tendsto f l (nhds x)) :
Filter.Tendsto (nhds f) l (nhds (nhds x))
theorem ContinuousWithinAt.nhds {X : Type u_4} {Y : Type u_5} [] [] {f : XY} {x : X} {s : Set X} (h : ) :
ContinuousWithinAt (nhds f) s x
theorem ContinuousAt.nhds {X : Type u_4} {Y : Type u_5} [] [] {f : XY} {x : X} (h : ) :
ContinuousAt (nhds f) x
theorem ContinuousOn.nhds {X : Type u_4} {Y : Type u_5} [] [] {f : XY} {s : Set X} (h : ) :
ContinuousOn (nhds f) s
theorem Continuous.nhds {X : Type u_4} {Y : Type u_5} [] [] {f : XY} (h : ) :
Continuous (nhds f)