mathlib documentation

topology.filter

Topology on the set of filters on a type #

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.

Tags #

filter, topological space

@[protected, instance]

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_set_of_mem {α : Type u_2} {s : set α} :
is_open {l : filter α | s l}
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 α) :
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]

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} :
@[simp]
theorem filter.nhds_top {α : Type u_2} :
@[simp]
theorem filter.nhds_pure {α : Type u_2} (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 α) :
@[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} :
@[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
@[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))
@[continuity]
@[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)) :
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) :
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) :
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) :
theorem continuous.nhds {X : Type u_4} {Y : Type u_5} [topological_space X] [topological_space Y] {f : X Y} (h : continuous f) :