mathlib documentation

topology.basic

Basic theory of topological spaces.

The main definition is the type class topological space α which endows a type α with a topology. Then set α gets predicates is_open, is_closed and functions interior, closure and frontier. Each point x of α gets a neighborhood filter 𝓝 x. A filter F on α has x as a cluster point if is_cluster_pt x F : 𝓝 x ⊓ F ≠ ⊥. A map f : ι → α clusters at x along F : filter ι if map_cluster_pt x F f : cluster_pt x (map f F). In particular the notion of cluster point of a sequence u is map_cluster_pt x at_top u.

This file also defines locally finite families of subsets of α.

For topological spaces α and β, a function f : α → β and a point a : α, continuous_at f a means f is continuous at a, and global continuity is continuous f. There is also a version of continuity pcontinuous for partially defined functions.

Notation

Implementation notes

Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in https://leanprover-community.github.io/theories/topology.html.

References

Tags

topological space, interior, closure, frontier, neighborhood, continuity, continuous function

 Topological spaces

@[class]
structure topological_space  :
Type uType u

A topology on α.

Instances
def topological_space.of_closed {α : Type u} (T : set (set α)) :
T(∀ (A : set (set α)), A T⋂₀A T)(∀ (A B : set α), A TB TA B T)topological_space α

A constructor for topologies by specifying the closed sets, and showing that they satisfy the appropriate conditions.

Equations
@[ext]
theorem topological_space_eq {α : Type u} {f g : topological_space α} :
f.is_open = g.is_openf = g

def is_open {α : Type u} [t : topological_space α] :
set α → Prop

is_open s means that s is open in the ambient topological space on α

Equations
@[simp]
theorem is_open_univ {α : Type u} [t : topological_space α] :

theorem is_open_inter {α : Type u} {s₁ s₂ : set α} [t : topological_space α] :
is_open s₁is_open s₂is_open (s₁ s₂)

theorem is_open_sUnion {α : Type u} [t : topological_space α] {s : set (set α)} :
(∀ (t_1 : set α), t_1 sis_open t_1)is_open (⋃₀s)

theorem is_open_fold {α : Type u} {s : set α} {t : topological_space α} :

theorem is_open_Union {α : Type u} {ι : Sort w} [topological_space α] {f : ι → set α} :
(∀ (i : ι), is_open (f i))is_open (⋃ (i : ι), f i)

theorem is_open_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} :
(∀ (i : β), i sis_open (f i))is_open (⋃ (i : β) (H : i s), f i)

theorem is_open_union {α : Type u} {s₁ s₂ : set α} [topological_space α] :
is_open s₁is_open s₂is_open (s₁ s₂)

@[simp]
theorem is_open_empty {α : Type u} [topological_space α] :

theorem is_open_sInter {α : Type u} [topological_space α] {s : set (set α)} :
s.finite(∀ (t : set α), t sis_open t)is_open (⋂₀s)

theorem is_open_bInter {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} :
s.finite(∀ (i : β), i sis_open (f i))is_open (⋂ (i : β) (H : i s), f i)

theorem is_open_Inter {α : Type u} {β : Type v} [topological_space α] [fintype β] {s : β → set α} :
(∀ (i : β), is_open (s i))is_open (⋂ (i : β), s i)

theorem is_open_Inter_prop {α : Type u} [topological_space α] {p : Prop} {s : p → set α} :
(∀ (h : p), is_open (s h))is_open (set.Inter s)

theorem is_open_const {α : Type u} [topological_space α] {p : Prop} :
is_open {a : α | p}

theorem is_open_and {α : Type u} {p₁ p₂ : α → Prop} [topological_space α] :
is_open {a : α | p₁ a}is_open {a : α | p₂ a}is_open {a : α | p₁ a p₂ a}

def is_closed {α : Type u} [topological_space α] :
set α → Prop

A set is closed if its complement is open

Equations
@[simp]
theorem is_closed_empty {α : Type u} [topological_space α] :

@[simp]
theorem is_closed_univ {α : Type u} [topological_space α] :

theorem is_closed_union {α : Type u} {s₁ s₂ : set α} [topological_space α] :
is_closed s₁is_closed s₂is_closed (s₁ s₂)

theorem is_closed_sInter {α : Type u} [topological_space α] {s : set (set α)} :
(∀ (t : set α), t sis_closed t)is_closed (⋂₀s)

theorem is_closed_Inter {α : Type u} {ι : Sort w} [topological_space α] {f : ι → set α} :
(∀ (i : ι), is_closed (f i))is_closed (⋂ (i : ι), f i)

@[simp]
theorem is_open_compl_iff {α : Type u} [topological_space α] {s : set α} :

@[simp]
theorem is_closed_compl_iff {α : Type u} [topological_space α] {s : set α} :

theorem is_open_diff {α : Type u} [topological_space α] {s t : set α} :
is_open sis_closed tis_open (s \ t)

theorem is_closed_inter {α : Type u} {s₁ s₂ : set α} [topological_space α] :
is_closed s₁is_closed s₂is_closed (s₁ s₂)

theorem is_closed_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} :
s.finite(∀ (i : β), i sis_closed (f i))is_closed (⋃ (i : β) (H : i s), f i)

theorem is_closed_Union {α : Type u} {β : Type v} [topological_space α] [fintype β] {s : β → set α} :
(∀ (i : β), is_closed (s i))is_closed (set.Union s)

theorem is_closed_Union_prop {α : Type u} [topological_space α] {p : Prop} {s : p → set α} :
(∀ (h : p), is_closed (s h))is_closed (set.Union s)

theorem is_closed_imp {α : Type u} [topological_space α] {p q : α → Prop} :
is_open {x : α | p x}is_closed {x : α | q x}is_closed {x : α | p xq x}

theorem is_open_neg {α : Type u} {p : α → Prop} [topological_space α] :
is_closed {a : α | p a}is_open {a : α | ¬p a}

Interior of a set

def interior {α : Type u} [topological_space α] :
set αset α

The interior of a set s is the largest open subset of s.

Equations
theorem mem_interior {α : Type u} [topological_space α] {s : set α} {x : α} :
x interior s ∃ (t : set α) (H : t s), is_open t x t

@[simp]
theorem is_open_interior {α : Type u} [topological_space α] {s : set α} :

theorem interior_subset {α : Type u} [topological_space α] {s : set α} :

theorem interior_maximal {α : Type u} [topological_space α] {s t : set α} :
t sis_open tt interior s

theorem is_open.interior_eq {α : Type u} [topological_space α] {s : set α} :
is_open sinterior s = s

theorem interior_eq_iff_open {α : Type u} [topological_space α] {s : set α} :

theorem subset_interior_iff_open {α : Type u} [topological_space α] {s : set α} :

theorem subset_interior_iff_subset_of_open {α : Type u} [topological_space α] {s t : set α} :
is_open s(s interior t s t)

theorem interior_mono {α : Type u} [topological_space α] {s t : set α} :
s tinterior s interior t

@[simp]
theorem interior_empty {α : Type u} [topological_space α] :

@[simp]
theorem interior_univ {α : Type u} [topological_space α] :

@[simp]
theorem interior_interior {α : Type u} [topological_space α] {s : set α} :

@[simp]
theorem interior_inter {α : Type u} [topological_space α] {s t : set α} :

theorem interior_union_is_closed_of_interior_empty {α : Type u} [topological_space α] {s t : set α} :

theorem is_open_iff_forall_mem_open {α : Type u} {s : set α} [topological_space α] :
is_open s ∀ (x : α), x s(∃ (t : set α) (H : t s), is_open t x t)

 Closure of a set

def closure {α : Type u} [topological_space α] :
set αset α

The closure of s is the smallest closed set containing s.

Equations
@[simp]
theorem is_closed_closure {α : Type u} [topological_space α] {s : set α} :

theorem subset_closure {α : Type u} [topological_space α] {s : set α} :

theorem closure_minimal {α : Type u} [topological_space α] {s t : set α} :
s tis_closed tclosure s t

theorem is_closed.closure_eq {α : Type u} [topological_space α] {s : set α} :
is_closed sclosure s = s

theorem is_closed.closure_subset {α : Type u} [topological_space α] {s : set α} :

theorem is_closed.closure_subset_iff {α : Type u} [topological_space α] {s t : set α} :
is_closed t(closure s t s t)

theorem closure_mono {α : Type u} [topological_space α] {s t : set α} :
s tclosure s closure t

theorem monotone_closure (α : Type u_1) [topological_space α] :

theorem closure_inter_subset_inter_closure {α : Type u} [topological_space α] (s t : set α) :

theorem is_closed_of_closure_subset {α : Type u} [topological_space α] {s : set α} :

theorem closure_eq_iff_is_closed {α : Type u} [topological_space α] {s : set α} :

theorem closure_subset_iff_is_closed {α : Type u} [topological_space α] {s : set α} :

@[simp]
theorem closure_empty {α : Type u} [topological_space α] :

@[simp]
theorem closure_empty_iff {α : Type u} [topological_space α] (s : set α) :

theorem set.nonempty.closure {α : Type u} [topological_space α] {s : set α} :

@[simp]
theorem closure_univ {α : Type u} [topological_space α] :

@[simp]
theorem closure_closure {α : Type u} [topological_space α] {s : set α} :

@[simp]
theorem closure_union {α : Type u} [topological_space α] {s t : set α} :

theorem interior_subset_closure {α : Type u} [topological_space α] {s : set α} :

theorem closure_eq_compl_interior_compl {α : Type u} [topological_space α] {s : set α} :

@[simp]
theorem interior_compl {α : Type u} [topological_space α] {s : set α} :

@[simp]
theorem closure_compl {α : Type u} [topological_space α] {s : set α} :

theorem mem_closure_iff {α : Type u} [topological_space α] {s : set α} {a : α} :
a closure s ∀ (o : set α), is_open oa o(o s).nonempty

def dense {α : Type u} [topological_space α] :
set α → Prop

A set is dense in a topological space if every point belongs to its closure.

Equations
theorem dense_iff_closure_eq {α : Type u} [topological_space α] {s : set α} :

theorem dense.closure_eq {α : Type u} [topological_space α] {s : set α} :

@[simp]
theorem dense_closure {α : Type u} [topological_space α] {s : set α} :

The closure of a set s is dense if and only if s is dense.

@[simp]
theorem dense_univ {α : Type u} [topological_space α] :

theorem dense_iff_inter_open {α : Type u} [topological_space α] {s : set α} :
dense s ∀ (U : set α), is_open UU.nonempty(U s).nonempty

A set is dense if and only if it has a nonempty intersection with each nonempty open set.

theorem dense.nonempty_iff {α : Type u} [topological_space α] {s : set α} :
dense s(s.nonempty nonempty α)

theorem dense.nonempty {α : Type u} [topological_space α] [h : nonempty α] {s : set α} :
dense s → s.nonempty

theorem dense.mono {α : Type u} [topological_space α] {s₁ s₂ : set α} :
s₁ s₂dense s₁dense s₂

Frontier of a set

def frontier {α : Type u} [topological_space α] :
set αset α

The frontier of a set is the set of points between the closure and interior.

Equations
@[simp]
theorem frontier_compl {α : Type u} [topological_space α] (s : set α) :

The complement of a set has the same frontier as the original set.

theorem frontier_inter_subset {α : Type u} [topological_space α] (s t : set α) :

theorem is_closed.frontier_eq {α : Type u} [topological_space α] {s : set α} :

theorem is_open.frontier_eq {α : Type u} [topological_space α] {s : set α} :
is_open sfrontier s = closure s \ s

theorem is_closed_frontier {α : Type u} [topological_space α] {s : set α} :

The frontier of a set is closed.

theorem interior_frontier {α : Type u} [topological_space α] {s : set α} :

The frontier of a closed set has no interior point.

theorem closure_eq_self_union_frontier {α : Type u} [topological_space α] (s : set α) :

 Neighborhoods

def nhds {α : Type u} [topological_space α] :
α → filter α

A set is called a neighborhood of a if it contains an open set around a. The set of all neighborhoods of a forms a filter, the neighborhood filter at a, is here defined as the infimum over the principal filters of all open sets containing a.

Equations
theorem nhds_def {α : Type u} [topological_space α] (a : α) :
𝓝 a = ⨅ (s : set α) (H : s {s : set α | a s is_open s}), 𝓟 s

theorem nhds_basis_opens {α : Type u} [topological_space α] (a : α) :
(𝓝 a).has_basis (λ (s : set α), a s is_open s) (λ (x : set α), x)

The open sets containing a are a basis for the neighborhood filter. See nhds_basis_opens' for a variant using open neighborhoods instead.

theorem le_nhds_iff {α : Type u} [topological_space α] {f : filter α} {a : α} :
f 𝓝 a ∀ (s : set α), a sis_open ss f

A filter lies below the neighborhood filter at a iff it contains every open set around a.

theorem nhds_le_of_le {α : Type u} [topological_space α] {f : filter α} {a : α} {s : set α} :
a sis_open s𝓟 s f𝓝 a f

To show a filter is above the neighborhood filter at a, it suffices to show that it is above the principal filter of some open set s containing a.

theorem mem_nhds_sets_iff {α : Type u} [topological_space α] {a : α} {s : set α} :
s 𝓝 a ∃ (t : set α) (H : t s), is_open t a t

theorem eventually_nhds_iff {α : Type u} [topological_space α] {a : α} {p : α → Prop} :
(∀ᶠ (x : α) in 𝓝 a, p x) ∃ (t : set α), (∀ (x : α), x tp x) is_open t a t

A predicate is true in a neighborhood of a iff it is true for all the points in an open set containing a.

theorem map_nhds {α : Type u} {β : Type v} [topological_space α] {a : α} {f : α → β} :
filter.map f (𝓝 a) = ⨅ (s : set α) (H : s {s : set α | a s is_open s}), 𝓟 (f '' s)

theorem mem_of_nhds {α : Type u} [topological_space α] {a : α} {s : set α} :
s 𝓝 aa s

theorem filter.eventually.self_of_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} :
(∀ᶠ (y : α) in 𝓝 a, p y)p a

If a predicate is true in a neighborhood of a, then it is true for a.

theorem mem_nhds_sets {α : Type u} [topological_space α] {a : α} {s : set α} :
is_open sa ss 𝓝 a

theorem is_open.eventually_mem {α : Type u} [topological_space α] {a : α} {s : set α} :
is_open sa s(∀ᶠ (x : α) in 𝓝 a, x s)

theorem nhds_basis_opens' {α : Type u} [topological_space α] (a : α) :
(𝓝 a).has_basis (λ (s : set α), s 𝓝 a is_open s) (λ (x : set α), x)

The open neighborhoods of a are a basis for the neighborhood filter. See nhds_basis_opens for a variant using open sets around a instead.

theorem filter.eventually.eventually_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} :
(∀ᶠ (y : α) in 𝓝 a, p y)(∀ᶠ (y : α) in 𝓝 a, ∀ᶠ (x : α) in 𝓝 y, p x)

If a predicate is true in a neighbourhood of a, then for y sufficiently close to a this predicate is true in a neighbourhood of y.

@[simp]
theorem eventually_eventually_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} :
(∀ᶠ (y : α) in 𝓝 a, ∀ᶠ (x : α) in 𝓝 y, p x) ∀ᶠ (x : α) in 𝓝 a, p x

@[simp]
theorem nhds_bind_nhds {α : Type u} {a : α} [topological_space α] :

@[simp]
theorem eventually_eventually_eq_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} :
(∀ᶠ (y : α) in 𝓝 a, f =ᶠ[𝓝 y] g) f =ᶠ[𝓝 a] g

theorem filter.eventually_eq.eq_of_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} :
f =ᶠ[𝓝 a] gf a = g a

@[simp]
theorem eventually_eventually_le_nhds {α : Type u} {β : Type v} [topological_space α] [has_le β] {f g : α → β} {a : α} :
(∀ᶠ (y : α) in 𝓝 a, f ≤ᶠ[𝓝 y] g) f ≤ᶠ[𝓝 a] g

theorem filter.eventually_eq.eventually_eq_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} :
f =ᶠ[𝓝 a] g(∀ᶠ (y : α) in 𝓝 a, f =ᶠ[𝓝 y] g)

If two functions are equal in a neighbourhood of a, then for y sufficiently close to a these functions are equal in a neighbourhood of y.

theorem filter.eventually_le.eventually_le_nhds {α : Type u} {β : Type v} [topological_space α] [has_le β] {f g : α → β} {a : α} :
f ≤ᶠ[𝓝 a] g(∀ᶠ (y : α) in 𝓝 a, f ≤ᶠ[𝓝 y] g)

If f x ≤ g x in a neighbourhood of a, then for y sufficiently close to a we have f x ≤ g x in a neighbourhood of y.

theorem all_mem_nhds {α : Type u} [topological_space α] (x : α) (P : set α → Prop) :
(∀ (s t : set α), s tP sP t)((∀ (s : set α), s 𝓝 xP s) ∀ (s : set α), is_open sx sP s)

theorem all_mem_nhds_filter {α : Type u} {β : Type v} [topological_space α] (x : α) (f : set αset β) (hf : ∀ (s t : set α), s tf s f t) (l : filter β) :
(∀ (s : set α), s 𝓝 xf s l) ∀ (s : set α), is_open sx sf s l

theorem rtendsto_nhds {α : Type u} {β : Type v} [topological_space α] {r : rel β α} {l : filter β} {a : α} :
filter.rtendsto r l (𝓝 a) ∀ (s : set α), is_open sa sr.core s l

theorem rtendsto'_nhds {α : Type u} {β : Type v} [topological_space α] {r : rel β α} {l : filter β} {a : α} :
filter.rtendsto' r l (𝓝 a) ∀ (s : set α), is_open sa sr.preimage s l

theorem ptendsto_nhds {α : Type u} {β : Type v} [topological_space α] {f : β →. α} {l : filter β} {a : α} :
filter.ptendsto f l (𝓝 a) ∀ (s : set α), is_open sa sf.core s l

theorem ptendsto'_nhds {α : Type u} {β : Type v} [topological_space α] {f : β →. α} {l : filter β} {a : α} :
filter.ptendsto' f l (𝓝 a) ∀ (s : set α), is_open sa sf.preimage s l

theorem tendsto_nhds {α : Type u} {β : Type v} [topological_space α] {f : β → α} {l : filter β} {a : α} :
filter.tendsto f l (𝓝 a) ∀ (s : set α), is_open sa sf ⁻¹' s l

theorem tendsto_const_nhds {α : Type u} {β : Type v} [topological_space α] {a : α} {f : filter β} :
filter.tendsto (λ (b : β), a) f (𝓝 a)

theorem pure_le_nhds {α : Type u} [topological_space α] :

theorem tendsto_pure_nhds {β : Type v} {α : Type u_1} [topological_space β] (f : α → β) (a : α) :
filter.tendsto f (pure a) (𝓝 (f a))

theorem order_top.tendsto_at_top_nhds {β : Type v} {α : Type u_1} [order_top α] [topological_space β] (f : α → β) :

@[simp, instance]
def nhds_ne_bot {α : Type u} [topological_space α] {a : α} :

Cluster points

In this section we define cluster points (also known as limit points and accumulation points) of a filter and of a sequence.

def cluster_pt {α : Type u} [topological_space α] :
α → filter α → Prop

A point x is a cluster point of a filter F if 𝓝 x ⊓ F ≠ ⊥. Also known as an accumulation point or a limit point.

Equations
theorem cluster_pt.ne_bot {α : Type u} [topological_space α] {x : α} {F : filter α} :
cluster_pt x F(𝓝 x F).ne_bot

theorem cluster_pt_iff {α : Type u} [topological_space α] {x : α} {F : filter α} :
cluster_pt x F ∀ {U V : set α}, U 𝓝 xV F(U V).nonempty

theorem cluster_pt_principal_iff {α : Type u} [topological_space α] {x : α} {s : set α} :
cluster_pt x (𝓟 s) ∀ (U : set α), U 𝓝 x(U s).nonempty

x is a cluster point of a set s if every neighbourhood of x meets s on a nonempty set.

theorem cluster_pt_principal_iff_frequently {α : Type u} [topological_space α] {x : α} {s : set α} :
cluster_pt x (𝓟 s) ∃ᶠ (y : α) in 𝓝 x, y s

theorem cluster_pt.of_le_nhds {α : Type u} [topological_space α] {x : α} {f : filter α} (H : f 𝓝 x) [f.ne_bot] :

theorem cluster_pt.of_le_nhds' {α : Type u} [topological_space α] {x : α} {f : filter α} :
f 𝓝 xf.ne_botcluster_pt x f

theorem cluster_pt.of_nhds_le {α : Type u} [topological_space α] {x : α} {f : filter α} :
𝓝 x fcluster_pt x f

theorem cluster_pt.mono {α : Type u} [topological_space α] {x : α} {f g : filter α} :
cluster_pt x ff gcluster_pt x g

theorem cluster_pt.of_inf_left {α : Type u} [topological_space α] {x : α} {f g : filter α} :
cluster_pt x (f g)cluster_pt x f

theorem cluster_pt.of_inf_right {α : Type u} [topological_space α] {x : α} {f g : filter α} :
cluster_pt x (f g)cluster_pt x g

def map_cluster_pt {α : Type u} [topological_space α] {ι : Type u_1} :
α → filter ι(ι → α) → Prop

A point x is a cluster point of a sequence u along a filter F if it is a cluster point of map u F.

Equations
theorem map_cluster_pt_iff {α : Type u} [topological_space α] {ι : Type u_1} (x : α) (F : filter ι) (u : ι → α) :
map_cluster_pt x F u ∀ (s : set α), s 𝓝 x(∃ᶠ (a : ι) in F, u a s)

theorem map_cluster_pt_of_comp {α : Type u} [topological_space α] {ι : Type u_1} {δ : Type u_2} {F : filter ι} {φ : δ → ι} {p : filter δ} {x : α} {u : ι → α} [p.ne_bot] :
filter.tendsto φ p Ffilter.tendsto (u φ) p (𝓝 x)map_cluster_pt x F u

Interior, closure and frontier in terms of neighborhoods

theorem interior_eq_nhds {α : Type u} [topological_space α] {s : set α} :
interior s = {a : α | 𝓝 a 𝓟 s}

theorem mem_interior_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :

theorem subset_interior_iff_nhds {α : Type u} [topological_space α] {s V : set α} :
s interior V ∀ (x : α), x sV 𝓝 x

theorem is_open_iff_nhds {α : Type u} [topological_space α] {s : set α} :
is_open s ∀ (a : α), a s𝓝 a 𝓟 s

theorem is_open_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} :
is_open s ∀ (a : α), a ss 𝓝 a

theorem is_open_iff_ultrafilter {α : Type u} [topological_space α] {s : set α} :
is_open s ∀ (x : α), x s∀ (l : filter α), l.is_ultrafilterl 𝓝 xs l

theorem mem_closure_iff_frequently {α : Type u} [topological_space α] {s : set α} {a : α} :
a closure s ∃ᶠ (x : α) in 𝓝 a, x s

theorem mem_closure_iff_cluster_pt {α : Type u} [topological_space α] {s : set α} {a : α} :

theorem closure_eq_cluster_pts {α : Type u} [topological_space α] {s : set α} :
closure s = {a : α | cluster_pt a (𝓟 s)}

theorem mem_closure_iff_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
a closure s ∀ (t : set α), t 𝓝 a(t s).nonempty

theorem mem_closure_iff_nhds' {α : Type u} [topological_space α] {s : set α} {a : α} :
a closure s ∀ (t : set α), t 𝓝 a(∃ (y : s), y t)

theorem mem_closure_iff_comap_ne_bot {α : Type u} [topological_space α] {A : set α} {x : α} :

theorem mem_closure_iff_nhds_basis {α : Type u} {β : Type v} [topological_space α] {a : α} {p : β → Prop} {s : β → set α} (h : (𝓝 a).has_basis p s) {t : set α} :
a closure t ∀ (i : β), p i(∃ (y : α) (H : y t), y s i)

theorem mem_closure_iff_ultrafilter {α : Type u} [topological_space α] {s : set α} {x : α} :
x closure s ∃ (u : filter.ultrafilter α), s u.val u.val 𝓝 x

x belongs to the closure of s if and only if some ultrafilter supported on s converges to x.

theorem is_closed_iff_cluster_pt {α : Type u} [topological_space α] {s : set α} :
is_closed s ∀ (a : α), cluster_pt a (𝓟 s)a s

theorem is_closed_iff_nhds {α : Type u} [topological_space α] {s : set α} :
is_closed s ∀ (x : α), (∀ (U : set α), U 𝓝 x(U s).nonempty)x s

theorem closure_inter_open {α : Type u} [topological_space α] {s t : set α} :
is_open ss closure t closure (s t)

theorem dense.inter_of_open_left {α : Type u} [topological_space α] {s t : set α} :
dense sdense tis_open sdense (s t)

The intersection of an open dense set with a dense set is a dense set.

theorem dense.inter_of_open_right {α : Type u} [topological_space α] {s t : set α} :
dense sdense tis_open tdense (s t)

The intersection of a dense set with an open dense set is a dense set.

theorem closure_diff {α : Type u} [topological_space α] {s t : set α} :

theorem filter.frequently.mem_of_closed {α : Type u} [topological_space α] {a : α} {s : set α} :
(∃ᶠ (x : α) in 𝓝 a, x s)is_closed sa s

theorem is_closed.mem_of_frequently_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} :
is_closed s(∃ᶠ (x : β) in b, f x s)filter.tendsto f b (𝓝 a)a s

theorem is_closed.mem_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} [b.ne_bot] :
is_closed sfilter.tendsto f b (𝓝 a)(∀ᶠ (x : β) in b, f x s)a s

theorem mem_closure_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} [b.ne_bot] :
filter.tendsto f b (𝓝 a)(∀ᶠ (x : β) in b, f x s)a closure s

theorem tendsto_inf_principal_nhds_iff_of_forall_eq {α : Type u} {β : Type v} [topological_space α] {f : β → α} {l : filter β} {s : set β} {a : α} :
(∀ (x : β), x sf x = a)(filter.tendsto f (l 𝓟 s) (𝓝 a) filter.tendsto f l (𝓝 a))

Suppose that f sends the complement to s to a single point a, and l is some filter. Then f tends to a along l restricted to s if and only if it tends to a along l.

Limits of filters in topological spaces

def Lim {α : Type u} [topological_space α] [nonempty α] :
filter α → α

If f is a filter, then Lim f is a limit of the filter, if it exists.

Equations
def Lim' {α : Type u} [topological_space α] (f : filter α) [f.ne_bot] :
α

If f is a filter satisfying ne_bot f, then Lim' f is a limit of the filter, if it exists.

Equations
def filter.ultrafilter.Lim {α : Type u} [topological_space α] :

If F is an ultrafilter, then filter.ultrafilter.Lim F is a limit of the filter, if it exists. Note that dot notation F.Lim can be used for F : ultrafilter α.

Equations
def lim {α : Type u} {β : Type v} [topological_space α] [nonempty α] :
filter β(β → α) → α

If f is a filter in β and g : β → α is a function, then lim f is a limit of g at f, if it exists.

Equations
theorem le_nhds_Lim {α : Type u} [topological_space α] {f : filter α} (h : ∃ (a : α), f 𝓝 a) :
f 𝓝 (Lim f)

If a filter f is majorated by some 𝓝 a, then it is majorated by 𝓝 (Lim f). We formulate this lemma with a [nonempty α] argument of Lim derived from h to make it useful for types without a [nonempty α] instance. Because of the built-in proof irrelevance, Lean will unify this instance with any other instance.

theorem tendsto_nhds_lim {α : Type u} {β : Type v} [topological_space α] {f : filter β} {g : β → α} (h : ∃ (a : α), filter.tendsto g f (𝓝 a)) :
filter.tendsto g f (𝓝 (lim f g))

If g tends to some 𝓝 a along f, then it tends to 𝓝 (lim f g). We formulate this lemma with a [nonempty α] argument of lim derived from h to make it useful for types without a [nonempty α] instance. Because of the built-in proof irrelevance, Lean will unify this instance with any other instance.

 Locally finite families

def locally_finite {α : Type u} {β : Type v} [topological_space α] :
(β → set α) → Prop

A family of sets in set α is locally finite if at every point x:α, there is a neighborhood of x which meets only finitely many sets in the family

Equations
theorem locally_finite_of_finite {α : Type u} {β : Type v} [topological_space α] {f : β → set α} :

theorem locally_finite_subset {α : Type u} {β : Type v} [topological_space α] {f₁ f₂ : β → set α} :
locally_finite f₂(∀ (b : β), f₁ b f₂ b)locally_finite f₁

theorem is_closed_Union_of_locally_finite {α : Type u} {β : Type v} [topological_space α] {f : β → set α} :
locally_finite f(∀ (i : β), is_closed (f i))is_closed (⋃ (i : β), f i)

Continuity

def continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
(α → β) → Prop

A function between topological spaces is continuous if the preimage of every open set is open.

Equations
theorem is_open.preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set β} :
is_open sis_open (f ⁻¹' s)

def continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
(α → β)α → Prop

A function between topological spaces is continuous at a point x₀ if f x tends to f x₀ when x tends to x₀.

Equations
theorem continuous_at.tendsto {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} :
continuous_at f xfilter.tendsto f (𝓝 x) (𝓝 (f x))

theorem continuous_at.preimage_mem_nhds {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {t : set β} :
continuous_at f xt 𝓝 (f x)f ⁻¹' t 𝓝 x

theorem preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set β} :

theorem continuous_id {α : Type u_1} [topological_space α] :

theorem continuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} :

theorem continuous.iterate {α : Type u_1} [topological_space α] {f : α → α} (h : continuous f) (n : ) :

theorem continuous_at.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {x : α} :
continuous_at g (f x)continuous_at f xcontinuous_at (g f) x

theorem continuous.tendsto {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (x : α) :
filter.tendsto f (𝓝 x) (𝓝 (f x))

theorem continuous.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} :

theorem continuous_iff_continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ∀ (x : α), continuous_at f x

theorem continuous_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {b : β} :
continuous (λ (a : α), b)

theorem continuous_at_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {b : β} :
continuous_at (λ (a : α), b) x

theorem continuous_at_id {α : Type u_1} [topological_space α] {x : α} :

theorem continuous_at.iterate {α : Type u_1} [topological_space α] {f : α → α} {x : α} (hf : continuous_at f x) (hx : f x = x) (n : ) :

theorem continuous_iff_is_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ∀ (s : set β), is_closed sis_closed (f ⁻¹' s)

theorem is_closed.preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set β} :

theorem continuous_at_iff_ultrafilter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (x : α) :
continuous_at f x ∀ (g : filter α), g.is_ultrafilterg 𝓝 xfilter.map f g 𝓝 (f x)

theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ∀ (x : α) (g : filter α), g.is_ultrafilterg 𝓝 xfilter.map f g 𝓝 (f x)

theorem continuous_if {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {p : α → Prop} {f g : α → β} {h : Π (a : α), decidable (p a)} :
(∀ (a : α), a frontier {a : α | p a}f a = g a)continuous fcontinuous gcontinuous (λ (a : α), ite (p a) (f a) (g a))

A piecewise defined function if p then f else g is continuous, if both f and g are continuous, and they coincide on the frontier (boundary) of the set {a | p a}.

def pcontinuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :
→. β) → Prop

Continuity of a partial function

Equations
theorem open_dom_of_pcontinuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} :

theorem pcontinuous_iff' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} :
pcontinuous f ∀ {x : α} {y : β}, y f xfilter.ptendsto' f (𝓝 x) (𝓝 y)

theorem image_closure_subset_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :
continuous ff '' closure s closure (f '' s)

theorem mem_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {t : set β} {f : α → β} {a : α} :
continuous fa closure s(∀ (a : α), a sf a t)f a closure t

Function with dense range

def dense_range {β : Type u_2} [topological_space β] {κ : Type u_5} :
(κ → β) → Prop

f : ι → β has dense range if its range (image) is a dense subset of β.

Equations
theorem function.surjective.dense_range {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} :

A surjective map has dense range.

theorem dense_range_iff_closure_range {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} :

theorem dense_range.closure_range {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} :

theorem continuous.range_subset_closure_image_dense {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set α} :
dense sset.range f closure (f '' s)

theorem dense_range.dense_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf' : dense_range f) (hf : continuous f) {s : set α} :
dense sdense (f '' s)

The image of a dense set under a continuous map with dense range is a dense set.

theorem dense_range.dense_of_maps_to {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf' : dense_range f) (hf : continuous f) {s : set α} (hs : dense s) {t : set β} :
set.maps_to f s tdense t

If a continuous map with dense range maps a dense set to a subset of t, then t is a dense set.

theorem dense_range.comp {β : Type u_2} {γ : Type u_3} [topological_space β] [topological_space γ] {κ : Type u_5} {g : β → γ} {f : κ → β} :

Composition of a continuous map with dense range and a function with dense range has dense range.

theorem dense_range.nonempty_iff {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} :

theorem dense_range.nonempty {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} [h : nonempty β] :

def dense_range.some {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} :
dense_range fβ → κ

Given a function f : α → β with dense range and b : β, returns some a : α.

Equations