mathlib3 documentation

topology.filter

Topology on the set of filters on a type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file introduce 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.is_open_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.at_top whenever f tends to filter.at_top.
It turns filter X into a T₀ space and the order on filter X is the dual of the specialization_order (filter X).

Tags #

filter, topological space

@[protected, instance]

def filter.topological_space {α : Type u_2} :

topological_space (filter α)

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.is_open_iff.

Equations

filter.topological_space = topological_space.generate_from (set.range (set.Iic ∘ filter.principal))

theorem filter.is_open_Iic_principal {α : Type u_2} {s : set α} :

is_open (set.Iic (filter.principal s))

theorem filter.is_open_set_of_mem {α : Type u_2} {s : set α} :

is_open {l : filter α | s ∈ l}

theorem filter.is_topological_basis_Iic_principal {α : Type u_2} :

topological_space.is_topological_basis (set.range (set.Iic ∘ filter.principal))

theorem filter.is_open_iff {α : Type u_2} {s : set (filter α)} :

is_open s ↔ ∃ (T : set (set α)), s = ⋃ (t : set α) (H : t ∈ T), set.Iic (filter.principal t)

theorem filter.nhds_eq {α : Type u_2} (l : filter α) :

nhds l = l.lift' (set.Iic ∘ filter.principal)

theorem filter.nhds_eq' {α : Type u_2} (l : filter α) :

nhds l = l.lift' (λ (s : set α), {l' : filter α | s ∈ l'})

@[protected]

theorem filter.tendsto_nhds {α : Type u_2} {β : Type u_3} {la : filter α} {lb : filter β} {f : α → filter β} :

filter.tendsto f la (nhds lb) ↔ ∀ (s : set β), s ∈ lb → (∀ᶠ (a : α) in la, s ∈ f a)

theorem filter.has_basis.nhds {ι : Sort u_1} {α : Type u_2} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :

(nhds l).has_basis p (λ (i : ι), set.Iic (filter.principal (s i)))

@[protected, instance]

def filter.nhds.is_countably_generated {α : Type u_2} {l : filter α} [l.is_countably_generated] :

(nhds l).is_countably_generated

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

theorem filter.has_basis.nhds' {ι : Sort u_1} {α : Type u_2} {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :

(nhds l).has_basis p (λ (i : ι), {l' : filter α | s i ∈ l'})

theorem filter.mem_nhds_iff {α : Type u_2} {l : filter α} {S : set (filter α)} :

S ∈ nhds l ↔ ∃ (t : set α) (H : 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 : set α) (H : t ∈ l), ∀ ⦃l' : filter α⦄, t ∈ l' → l' ∈ S

@[simp]

theorem filter.nhds_bot {α : Type u_2} :

nhds ⊥ = has_pure.pure ⊥

@[simp]

theorem filter.nhds_top {α : Type u_2} :

@[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 (has_pure.pure x) = filter.principal {⊥, has_pure.pure x}

@[simp]

theorem filter.nhds_infi {ι : 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₁ l₂ : filter α) :

nhds (l₁ ⊓ l₂) = nhds l₁ ⊓ nhds l₂

theorem filter.monotone_nhds {α : Type u_2} :

theorem filter.Inter_nhds {α : Type u_2} (l : filter α) :

⋂₀ {s : set (filter α) | s ∈ nhds l} = set.Iic l

@[simp]

theorem filter.nhds_mono {α : Type u_2} {l₁ l₂ : filter α} :

nhds l₁ ≤ nhds l₂ ↔ l₁ ≤ l₂

@[protected]

theorem filter.mem_interior {α : Type u_2} {s : set (filter α)} {l : filter α} :

l ∈ interior s ↔ ∃ (t : set α) (H : t ∈ l), set.Iic (filter.principal t) ⊆ s

@[protected]

theorem filter.mem_closure {α : Type u_2} {s : set (filter α)} {l : filter α} :

l ∈ closure s ↔ ∀ (t : set α), t ∈ l → (∃ (l' : filter α) (H : l' ∈ s), t ∈ l')

@[protected, 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₁ l₂ : filter α} :

l₁ ⤳ l₂ ↔ l₁ ≤ l₂

@[protected, instance]

def filter.t0_space {α : Type u_2} :

t0_space (filter α)

theorem filter.nhds_at_top {α : Type u_2} [preorder α] :

nhds filter.at_top = ⨅ (x : α), filter.principal (set.Iic (filter.principal (set.Ici x)))

@[protected]

theorem filter.tendsto_nhds_at_top_iff {α : Type u_2} {β : Type u_3} [preorder β] {l : filter α} {f : α → filter β} :

filter.tendsto f l (nhds filter.at_top) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, set.Ici y ∈ f a

theorem filter.nhds_at_bot {α : Type u_2} [preorder α] :

nhds filter.at_bot = ⨅ (x : α), filter.principal (set.Iic (filter.principal (set.Iic x)))

@[protected]

theorem filter.tendsto_nhds_at_bot_iff {α : Type u_2} {β : Type u_3} [preorder β] {l : filter α} {f : α → filter β} :

filter.tendsto f l (nhds filter.at_bot) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, set.Iic y ∈ f a

theorem filter.nhds_nhds {X : Type u_4} [topological_space X] (x : X) :

nhds (nhds x) = ⨅ (s : set X) (hs : is_open s) (hx : x ∈ s), filter.principal (set.Iic (filter.principal s))

theorem filter.inducing_nhds {X : Type u_4} [topological_space X] :

@[continuity]

theorem filter.continuous_nhds {X : Type u_4} [topological_space X] :

continuous nhds

@[protected]

theorem filter.tendsto.nhds {α : Type u_2} {X : Type u_4} [topological_space X] {f : α → X} {l : filter α} {x : X} (h : filter.tendsto f l (nhds x)) :

filter.tendsto (nhds ∘ f) l (nhds (nhds x))

theorem continuous_within_at.nhds {X : Type u_4} {Y : Type u_5} [topological_space X] [topological_space Y] {f : X → Y} {x : X} {s : set X} (h : continuous_within_at f s x) :

continuous_within_at (nhds ∘ f) s x

theorem continuous_at.nhds {X : Type u_4} {Y : Type u_5} [topological_space X] [topological_space Y] {f : X → Y} {x : X} (h : continuous_at f x) :

continuous_at (nhds ∘ f) x

theorem continuous_on.nhds {X : Type u_4} {Y : Type u_5} [topological_space X] [topological_space Y] {f : X → Y} {s : set X} (h : continuous_on f s) :

continuous_on (nhds ∘ f) s

theorem continuous.nhds {X : Type u_4} {Y : Type u_5} [topological_space X] [topological_space Y] {f : X → Y} (h : continuous f) :

continuous (nhds ∘ f)