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} :

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
theorem filter.is_open_Iic_principal {α : Type u_2} {s : set α} :
theorem filter.is_open_set_of_mem {α : Type u_2} {s : set α} :
is_open {l : | s l}
theorem filter.is_open_iff {α : Type u_2} {s : set (filter α)} :
(T : set (set α)), s = (t : set α) (H : t T),
theorem filter.nhds_eq {α : Type u_2} (l : filter α) :
nhds l =
theorem filter.nhds_eq' {α : Type u_2} (l : filter α) :
nhds l = l.lift' (λ (s : set α), {l' : | s l'})
@[protected]
theorem filter.tendsto_nhds {α : Type u_2} {β : Type u_3} {la : filter α} {lb : filter β} {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 α}  :

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' : | s i l'})
theorem filter.mem_nhds_iff {α : Type u_2} {l : filter α} {S : set (filter α)} :
S nhds l (t : set α) (H : t l), S
theorem filter.mem_nhds_iff' {α : Type u_2} {l : filter α} {S : set (filter α)} :
S nhds l (t : set α) (H : 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_infi {ι : 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₂ : 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} =
@[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 (t : set α) (H : t l), s
@[protected]
theorem filter.mem_closure {α : Type u_2} {s : set (filter α)} {l : filter α} :
l (t : set α), t l ( (l' : filter α) (H : l' s), t l')
@[protected, simp]
theorem filter.closure_singleton {α : Type u_2} (l : filter α) :
closure {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} :
theorem filter.nhds_at_top {α : Type u_2} [preorder α] :
= (x : α),
@[protected]
theorem filter.tendsto_nhds_at_top_iff {α : Type u_2} {β : Type u_3} [preorder β] {l : filter α} {f : α } :
(y : β), ∀ᶠ (a : α) in l, f a
theorem filter.nhds_at_bot {α : Type u_2} [preorder α] :
= (x : α),
@[protected]
theorem filter.tendsto_nhds_at_bot_iff {α : Type u_2} {β : Type u_3} [preorder β] {l : filter α} {f : α } :
(y : β), ∀ᶠ (a : α) in l, f a
theorem filter.nhds_nhds {X : Type u_4} (x : X) :
nhds (nhds x) = (s : set X) (hs : is_open s) (hx : x s),
theorem filter.inducing_nhds {X : Type u_4}  :
@[continuity]
theorem filter.continuous_nhds {X : Type u_4}  :
@[protected]
theorem filter.tendsto.nhds {α : Type u_2} {X : Type u_4} {f : α X} {l : filter α} {x : X} (h : (nhds x)) :
theorem continuous_within_at.nhds {X : Type u_4} {Y : Type u_5} {f : X Y} {x : X} {s : set X} (h : x) :
s x
theorem continuous_at.nhds {X : Type u_4} {Y : Type u_5} {f : X Y} {x : X} (h : x) :
theorem continuous_on.nhds {X : Type u_4} {Y : Type u_5} {f : X Y} {s : set X} (h : s) :
theorem continuous.nhds {X : Type u_4} {Y : Type u_5} {f : X Y} (h : continuous f) :