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

instance Filter.instTopologicalSpaceFilter {α : Type u_2} : TopologicalSpace (Filter α)

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

• Filter.instTopologicalSpaceFilter = TopologicalSpace.generateFrom (Set.range (Set.Iic ∘ Filter.principal))

theorem Filter.isOpen_Iic_principal {α : Type u_2} {s : Set α} : IsOpen (Set.Iic (Filter.principal s))

theorem Filter.isOpen_setOf_mem {α : Type u_2} {s : Set α} : IsOpen {l : Filter α | s ∈ l}

theorem Filter.isTopologicalBasis_Iic_principal {α : Type u_2} : TopologicalSpace.IsTopologicalBasis (Set.range (Set.Iic ∘ Filter.principal))

theorem Filter.isOpen_iff {α : Type u_2} {s : Set (Filter α)} : IsOpen s ↔ ∃ (T : Set (Set α)), s = ⋃ t ∈ T, Set.Iic (Filter.principal t)

theorem Filter.nhds_eq {α : Type u_2} (l : Filter α) : nhds l = Filter.lift' l (Set.Iic ∘ Filter.principal)

theorem Filter.nhds_eq' {α : Type u_2} (l : Filter α) : nhds l = Filter.lift' l fun (s : Set α) => {l' : Filter α | s ∈ l'}

theorem Filter.tendsto_nhds {α : Type u_2} {β : Type u_3} {la : Filter α} {lb : Filter β} {f : α → Filter β} : Filter.Tendsto f la (nhds lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a

theorem Filter.HasBasis.nhds {ι : Sort u_1} {α : Type u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.HasBasis (nhds l) p fun (i : ι) => Set.Iic (Filter.principal (s i))

theorem Filter.tendsto_pure_self {X : Type u_4} (l : Filter X) : Filter.Tendsto pure l (nhds l)

instance Filter.instIsCountablyGeneratedFilterNhds {α : Type u_2} {l : Filter α} [Filter.IsCountablyGenerated l] : Filter.IsCountablyGenerated (nhds l)

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

Equations

• (_ : Filter.IsCountablyGenerated (nhds l)) = (_ : Filter.IsCountablyGenerated (nhds l))

theorem Filter.HasBasis.nhds' {ι : Sort u_1} {α : Type u_2} {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.HasBasis (nhds l) p fun (i : ι) => {l' : Filter α | s i ∈ l'}

theorem Filter.mem_nhds_iff {α : Type u_2} {l : Filter α} {S : Set (Filter α)} : S ∈ nhds l ↔ ∃ t ∈ l, Set.Iic (Filter.principal t) ⊆ S

theorem Filter.mem_nhds_iff' {α : Type u_2} {l : Filter α} {S : Set (Filter α)} : S ∈ nhds l ↔ ∃ t ∈ l, ∀ ⦃l' : Filter α⦄, t ∈ l' → l' ∈ S

@[simp]

theorem Filter.nhds_bot {α : Type u_2} : nhds ⊥ = pure ⊥

@[simp]

theorem Filter.nhds_top {α : Type u_2} : nhds ⊤ = ⊤

@[simp]

theorem Filter.nhds_principal {α : Type u_2} (s : Set α) : nhds (Filter.principal s) = Filter.principal (Set.Iic (Filter.principal s))

@[simp]

theorem Filter.nhds_pure {α : Type u_2} (x : α) : nhds (pure x) = Filter.principal {⊥, pure x}

@[simp]

theorem Filter.nhds_iInf {ι : Sort u_1} {α : Type u_2} (f : ι → Filter α) : nhds (⨅ (i : ι), f i) = ⨅ (i : ι), nhds (f i)

@[simp]

theorem Filter.nhds_inf {α : Type u_2} (l₁ : Filter α) (l₂ : Filter α) : nhds (l₁ ⊓ l₂) = nhds l₁ ⊓ nhds l₂

theorem Filter.monotone_nhds {α : Type u_2} : Monotone nhds

theorem Filter.sInter_nhds {α : Type u_2} (l : Filter α) : ⋂₀ {s : Set (Filter α) | s ∈ nhds l} = Set.Iic l

@[simp]

theorem Filter.nhds_mono {α : Type u_2} {l₁ : Filter α} {l₂ : Filter α} : nhds l₁ ≤ nhds l₂ ↔ l₁ ≤ l₂

theorem Filter.mem_interior {α : Type u_2} {s : Set (Filter α)} {l : Filter α} : l ∈ interior s ↔ ∃ t ∈ l, Set.Iic (Filter.principal t) ⊆ s

theorem Filter.mem_closure {α : Type u_2} {s : Set (Filter α)} {l : Filter α} : l ∈ closure s ↔ ∀ t ∈ l, ∃ l' ∈ s, t ∈ l'

@[simp]

theorem Filter.closure_singleton {α : Type u_2} (l : Filter α) : closure {l} = Set.Ici l

@[simp]

theorem Filter.specializes_iff_le {α : Type u_2} {l₁ : Filter α} {l₂ : Filter α} : l₁ ⤳ l₂ ↔ l₁ ≤ l₂

instance Filter.instT0SpaceFilterInstTopologicalSpaceFilter {α : Type u_2} : T0Space (Filter α)

Equations

• (_ : T0Space (Filter α)) = (_ : T0Space (Filter α))

theorem Filter.nhds_atTop {α : Type u_2} [Preorder α] : nhds Filter.atTop = ⨅ (x : α), Filter.principal (Set.Iic (Filter.principal (Set.Ici x)))

theorem Filter.tendsto_nhds_atTop_iff {α : Type u_2} {β : Type u_3} [Preorder β] {l : Filter α} {f : α → Filter β} : Filter.Tendsto f l (nhds Filter.atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Set.Ici y ∈ f a

theorem Filter.nhds_atBot {α : Type u_2} [Preorder α] : nhds Filter.atBot = ⨅ (x : α), Filter.principal (Set.Iic (Filter.principal (Set.Iic x)))

theorem Filter.tendsto_nhds_atBot_iff {α : Type u_2} {β : Type u_3} [Preorder β] {l : Filter α} {f : α → Filter β} : Filter.Tendsto f l (nhds Filter.atBot) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Set.Iic y ∈ f a

theorem Filter.nhds_nhds {X : Type u_4} [TopologicalSpace X] (x : X) : nhds (nhds x) = ⨅ (s : Set X), ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), Filter.principal (Set.Iic (Filter.principal s))

theorem Filter.inducing_nhds {X : Type u_4} [TopologicalSpace X] : Inducing nhds

theorem Filter.continuous_nhds {X : Type u_4} [TopologicalSpace X] : Continuous nhds

theorem Filter.Tendsto.nhds {α : Type u_2} {X : Type u_4} [TopologicalSpace X] {f : α → X} {l : Filter α} {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} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {s : Set X} (h : ContinuousWithinAt f s x) : ContinuousWithinAt (nhds ∘ f) s x

theorem ContinuousAt.nhds {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (h : ContinuousAt f x) : ContinuousAt (nhds ∘ f) x

theorem ContinuousOn.nhds {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (h : ContinuousOn f s) : ContinuousOn (nhds ∘ f) s

theorem Continuous.nhds {X : Type u_4} {Y : Type u_5} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (h : Continuous f) : Continuous (nhds ∘ f)