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

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 u) :
Type u

A topology on α.

Instances of this typeclass
Instances of other typeclasses for topological_space
def topological_space.of_closed {α : Type u} (T : set (set α)) (empty_mem : T) (sInter_mem : ∀ (A : set (set α)), A T⋂₀ A T) (union_mem : ∀ (A : set α), A T∀ (B : set α), B TA B T) :

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} [topological_space α] (s : set α) :
Prop

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

Equations
@[simp]
theorem is_open_univ {α : Type u} [topological_space α] :
theorem is_open.inter {α : Type u} {s₁ s₂ : set α} [topological_space α] (h₁ : is_open s₁) (h₂ : is_open s₂) :
is_open (s₁ s₂)
theorem is_open_sUnion {α : Type u} [topological_space α] {s : set (set α)} (h : ∀ (t : set α), t sis_open t) :
theorem topological_space_eq_iff {α : Type u} {t t' : topological_space α} :
t = t' ∀ (s : set α), is_open s 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 α} (h : ∀ (i : ι), is_open (f i)) :
is_open (⋃ (i : ι), f i)
theorem is_open_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (h : ∀ (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 α] (h₁ : is_open s₁) (h₂ : 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 α)} (hs : 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 α} (hs : 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 α] [finite β] {s : β → set α} (h : ∀ (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 : ∀ (h : p), is_open (s h)) :
theorem is_open_bInter_finset {α : Type u} {β : Type v} [topological_space α] {s : finset β} {f : β → set α} (h : ∀ (i : β), i sis_open (f i)) :
is_open (⋂ (i : β) (H : i s), f i)
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}
@[class]
structure is_closed {α : Type u} [topological_space α] (s : set α) :
Prop

A set is closed if its complement is open

Instances of this typeclass
@[simp]
theorem is_open_compl_iff {α : Type u} [topological_space α] {s : set α} :
@[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 α} (h : ∀ (i : ι), is_closed (f i)) :
is_closed (⋂ (i : ι), f i)
theorem is_closed_bInter {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (h : ∀ (i : β), i sis_closed (f i)) :
is_closed (⋂ (i : β) (H : i s), f i)
@[simp]
theorem is_closed_compl_iff {α : Type u} [topological_space α] {s : set α} :
theorem is_open.is_closed_compl {α : Type u} [topological_space α] {s : set α} (hs : is_open s) :
theorem is_open.sdiff {α : Type u} [topological_space α] {s t : set α} (h₁ : is_open s) (h₂ : is_closed t) :
is_open (s \ t)
theorem is_closed.inter {α : Type u} {s₁ s₂ : set α} [topological_space α] (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
is_closed (s₁ s₂)
theorem is_closed.sdiff {α : Type u} [topological_space α] {s t : set α} (h₁ : is_closed s) (h₂ : is_open t) :
is_closed (s \ t)
theorem is_closed_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (hs : 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 α] [finite β] {s : β → set α} (h : ∀ (i : β), is_closed (s i)) :
is_closed (⋃ (i : β), s i)
theorem is_closed_Union_prop {α : Type u} [topological_space α] {p : Prop} {s : p → set α} (h : ∀ (h : p), is_closed (s h)) :
theorem is_closed_imp {α : Type u} [topological_space α] {p q : α → Prop} (hp : is_open {x : α | p x}) (hq : is_closed {x : α | q x}) :
is_closed {x : α | p xq x}
theorem is_closed.not {α : 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 α] (s : 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 α} (h₁ : t s) (h₂ : is_open t) :
theorem is_open.interior_eq {α : Type u} [topological_space α] {s : set α} (h : is_open 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 α} (h₁ : is_open s) :
theorem subset_interior_iff {α : Type u} [topological_space α] {s t : set α} :
t interior s ∃ (U : set α), is_open U t U U s
theorem interior_mono {α : Type u} [topological_space α] {s t : set α} (h : s t) :
@[simp]
theorem interior_empty {α : Type u} [topological_space α] :
@[simp]
theorem interior_univ {α : Type u} [topological_space α] :
@[simp]
theorem interior_eq_univ {α : Type u} [topological_space α] {s : set α} :
@[simp]
theorem interior_interior {α : Type u} [topological_space α] {s : set α} :
@[simp]
theorem interior_inter {α : Type u} [topological_space α] {s t : set α} :
@[simp]
theorem finset.interior_Inter {α : Type u} [topological_space α] {ι : Type u_1} (s : finset ι) (f : ι → set α) :
interior (⋂ (i : ι) (H : i s), f i) = ⋂ (i : ι) (H : i s), interior (f i)
@[simp]
theorem interior_Inter {α : Type u} [topological_space α] {ι : Type u_1} [finite ι] (f : ι → set α) :
interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
theorem interior_union_is_closed_of_interior_empty {α : Type u} [topological_space α] {s t : set α} (h₁ : is_closed s) (h₂ : interior t = ) :
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)
theorem interior_Inter_subset {α : Type u} {ι : Sort w} [topological_space α] (s : ι → set α) :
interior (⋂ (i : ι), s i) ⋂ (i : ι), interior (s i)
theorem interior_Inter₂_subset {α : Type u} {ι : Sort w} [topological_space α] (p : ι → Sort u_1) (s : Π (i : ι), p iset α) :
interior (⋂ (i : ι) (j : p i), s i j) ⋂ (i : ι) (j : p i), interior (s i j)
theorem interior_sInter_subset {α : Type u} [topological_space α] (S : set (set α)) :
interior (⋂₀ S) ⋂ (s : set α) (H : s S), interior s

Closure of a set #

def closure {α : Type u} [topological_space α] (s : 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 not_mem_of_not_mem_closure {α : Type u} [topological_space α] {s : set α} {P : α} (hP : P closure s) :
P s
theorem closure_minimal {α : Type u} [topological_space α] {s t : set α} (h₁ : s t) (h₂ : is_closed t) :
theorem disjoint.closure_left {α : Type u} [topological_space α] {s t : set α} (hd : disjoint s t) (ht : is_open t) :
theorem disjoint.closure_right {α : Type u} [topological_space α] {s t : set α} (hd : disjoint s t) (hs : is_open s) :
theorem is_closed.closure_eq {α : Type u} [topological_space α] {s : set α} (h : is_closed s) :
theorem is_closed.closure_subset {α : Type u} [topological_space α] {s : set α} (hs : is_closed s) :
theorem is_closed.closure_subset_iff {α : Type u} [topological_space α] {s t : set α} (h₁ : is_closed t) :
closure s t s t
theorem is_closed.mem_iff_closure_subset {α : Type u_1} [topological_space α] {U : set α} (hU : is_closed U) {x : α} :
x U closure {x} U
theorem closure_mono {α : Type u} [topological_space α] {s t : set α} (h : s t) :
theorem monotone_closure (α : Type u_1) [topological_space α] :
theorem diff_subset_closure_iff {α : Type u} [topological_space α] {s t : set α} :
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 α} (h : closure s s) :
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 α) :
@[simp]
theorem closure_nonempty_iff {α : Type u} [topological_space α] {s : set α} :
theorem set.nonempty.of_closure {α : Type u} [topological_space α] {s : set α} :

Alias of the forward direction of closure_nonempty_iff.

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

Alias of the reverse direction of closure_nonempty_iff.

@[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 α} :
@[simp]
theorem finset.closure_bUnion {α : Type u} [topological_space α] {ι : Type u_1} (s : finset ι) (f : ι → set α) :
closure (⋃ (i : ι) (H : i s), f i) = ⋃ (i : ι) (H : i s), closure (f i)
@[simp]
theorem closure_Union {α : Type u} [topological_space α] {ι : Type u_1} [finite ι] (f : ι → set α) :
closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
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
theorem filter.le_lift'_closure {α : Type u} [topological_space α] (l : filter α) :
theorem filter.has_basis.lift'_closure {α : Type u} {ι : Sort w} [topological_space α] {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) :
(l.lift' closure).has_basis p (λ (i : ι), closure (s i))
theorem filter.has_basis.lift'_closure_eq_self {α : Type u} {ι : Sort w} [topological_space α] {l : filter α} {p : ι → Prop} {s : ι → set α} (h : l.has_basis p s) (hc : ∀ (i : ι), p iis_closed (s i)) :
def dense {α : Type u} [topological_space α] (s : 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 α} (h : dense s) :
theorem dense.interior_compl {α : Type u} [topological_space α] {s : set α} (h : dense s) :
@[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.

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

Alias of the forward direction of dense_closure.

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

Alias of the reverse direction of dense_closure.

@[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.inter_open_nonempty {α : Type u} [topological_space α] {s : set α} :
dense s∀ (U : set α), is_open UU.nonempty(U s).nonempty

Alias of the forward direction of dense_iff_inter_open.

theorem dense.exists_mem_open {α : Type u} [topological_space α] {s : set α} (hs : dense s) {U : set α} (ho : is_open U) (hne : U.nonempty) :
∃ (x : α) (H : x s), x U
theorem dense.nonempty_iff {α : Type u} [topological_space α] {s : set α} (hs : dense s) :
theorem dense.nonempty {α : Type u} [topological_space α] [h : nonempty α] {s : set α} (hs : dense s) :
theorem dense.mono {α : Type u} [topological_space α] {s₁ s₂ : set α} (h : s₁ s₂) (hd : dense s₁) :
dense s₂
theorem dense_compl_singleton_iff_not_open {α : Type u} [topological_space α] {x : α} :

Complement to a singleton is dense if and only if the singleton is not an open set.

Frontier of a set #

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

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

Equations
@[simp]
theorem closure_diff_interior {α : Type u} [topological_space α] (s : set α) :
@[simp]
theorem closure_diff_frontier {α : Type u} [topological_space α] (s : set α) :
@[simp]
theorem self_diff_frontier {α : Type u} [topological_space α] (s : set α) :
theorem frontier_subset_closure {α : Type u} [topological_space α] {s : set α} :
theorem is_closed.frontier_subset {α : Type u} {s : set α} [topological_space α] (hs : is_closed s) :
theorem frontier_closure_subset {α : Type u} [topological_space α] {s : set α} :
theorem frontier_interior_subset {α : Type u} [topological_space α] {s : set α} :
@[simp]
theorem frontier_compl {α : Type u} [topological_space α] (s : set α) :

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

@[simp]
theorem frontier_univ {α : Type u} [topological_space α] :
@[simp]
theorem frontier_empty {α : Type u} [topological_space α] :
theorem frontier_inter_subset {α : Type u} [topological_space α] (s t : set α) :
theorem is_closed.frontier_eq {α : Type u} [topological_space α] {s : set α} (hs : is_closed s) :
theorem is_open.frontier_eq {α : Type u} [topological_space α] {s : set α} (hs : is_open s) :
theorem is_open.inter_frontier_eq {α : Type u} [topological_space α] {s : set α} (hs : is_open 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 α} (h : is_closed s) :

The frontier of a closed set has no interior point.

theorem closure_eq_self_union_frontier {α : Type u} [topological_space α] (s : set α) :
theorem disjoint.frontier_left {α : Type u} {s t : set α} [topological_space α] (ht : is_open t) (hd : disjoint s t) :
theorem disjoint.frontier_right {α : Type u} {s t : set α} [topological_space α] (hs : is_open s) (hd : disjoint s t) :

Neighborhoods #

@[irreducible]
def nhds {α : Type u} [topological_space α] (a : α) :

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
Instances for nhds
theorem nhds_def {α : Type u} [topological_space α] (a : α) :
nhds a = ⨅ (s : set α) (H : s {s : set α | a s is_open s}), filter.principal s
theorem nhds_def' {α : Type u} [topological_space α] (a : α) :
nhds a = ⨅ (s : set α) (hs : is_open s) (ha : a s), filter.principal s
theorem nhds_basis_opens {α : Type u} [topological_space α] (a : α) :
(nhds a).has_basis (λ (s : set α), a s is_open s) (λ (s : set α), s)

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

theorem nhds_basis_closeds {α : Type u} [topological_space α] (a : α) :
(nhds a).has_basis (λ (s : set α), a s is_closed s) has_compl.compl
theorem le_nhds_iff {α : Type u} [topological_space α] {f : filter α} {a : α} :
f nhds 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 α} (h : a s) (o : is_open s) (sf : filter.principal s f) :
nhds 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_iff {α : Type u} [topological_space α] {a : α} {s : set α} :
s nhds a ∃ (t : set α) (H : t s), is_open t a t
theorem eventually_nhds_iff {α : Type u} [topological_space α] {a : α} {p : α → Prop} :
(∀ᶠ (x : α) in nhds 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 (nhds a) = ⨅ (s : set α) (H : s {s : set α | a s is_open s}), filter.principal (f '' s)
theorem mem_of_mem_nhds {α : Type u} [topological_space α] {a : α} {s : set α} :
s nhds aa s
theorem filter.eventually.self_of_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} (h : ∀ᶠ (y : α) in nhds a, p y) :
p a

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

theorem is_open.mem_nhds {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_open s) (ha : a s) :
s nhds a
theorem is_open.mem_nhds_iff {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_open s) :
s nhds a a s
theorem is_closed.compl_mem_nhds {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_closed s) (ha : a s) :
theorem is_open.eventually_mem {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_open s) (ha : a s) :
∀ᶠ (x : α) in nhds a, x s
theorem nhds_basis_opens' {α : Type u} [topological_space α] (a : α) :
(nhds a).has_basis (λ (s : set α), s nhds 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 exists_open_set_nhds {α : Type u} [topological_space α] {s U : set α} (h : ∀ (x : α), x sU nhds x) :
∃ (V : set α), s V is_open V V U

If U is a neighborhood of each point of a set s then it is a neighborhood of s: it contains an open set containing s.

theorem exists_open_set_nhds' {α : Type u} [topological_space α] {s U : set α} (h : U ⨆ (x : α) (H : x s), nhds x) :
∃ (V : set α), s V is_open V V U

If U is a neighborhood of each point of a set s then it is a neighborhood of s: it contains an open set containing s.

theorem filter.eventually.eventually_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} (h : ∀ᶠ (y : α) in nhds a, p y) :
∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhds 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 nhds a, ∀ᶠ (x : α) in nhds y, p x) ∀ᶠ (x : α) in nhds a, p x
@[simp]
theorem eventually_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
(∀ᶠ (x : α) in nhds a, s nhds x) s nhds a
@[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 nhds a, f =ᶠ[nhds y] g) f =ᶠ[nhds a] g
theorem filter.eventually_eq.eq_of_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} (h : f =ᶠ[nhds a] g) :
f a = g a
@[simp]
theorem eventually_eventually_le_nhds {α : Type u} {β : Type v} [topological_space α] [has_le β] {f g : α → β} {a : α} :
(∀ᶠ (y : α) in nhds a, f ≤ᶠ[nhds y] g) f ≤ᶠ[nhds a] g
theorem filter.eventually_eq.eventually_eq_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} (h : f =ᶠ[nhds a] g) :
∀ᶠ (y : α) in nhds a, f =ᶠ[nhds 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 : α} (h : f ≤ᶠ[nhds a] g) :
∀ᶠ (y : α) in nhds a, f ≤ᶠ[nhds 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) (hP : ∀ (s t : set α), s tP sP t) :
(∀ (s : set α), s nhds 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 nhds 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 (nhds 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 (nhds 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 (nhds 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 (nhds 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 (nhds a) ∀ (s : set α), is_open sa sf ⁻¹' s l
theorem tendsto_at_top_nhds {α : Type u} {β : Type v} [topological_space α] [nonempty β] [semilattice_sup β] {f : β → α} {a : α} :
filter.tendsto f filter.at_top (nhds a) ∀ (U : set α), a Uis_open U(∃ (N : β), ∀ (n : β), N nf n U)
theorem tendsto_const_nhds {α : Type u} {β : Type v} [topological_space α] {a : α} {f : filter β} :
filter.tendsto (λ (b : β), a) f (nhds a)
theorem tendsto_at_top_of_eventually_const {α : Type u} [topological_space α] {ι : Type u_1} [semilattice_sup ι] [nonempty ι] {x : α} {u : ι → α} {i₀ : ι} (h : ∀ (i : ι), i i₀u i = x) :
theorem tendsto_at_bot_of_eventually_const {α : Type u} [topological_space α] {ι : Type u_1} [semilattice_inf ι] [nonempty ι] {x : α} {u : ι → α} {i₀ : ι} (h : ∀ (i : ι), i i₀u i = x) :
theorem pure_le_nhds {α : Type u} [topological_space α] :
theorem tendsto_pure_nhds {β : Type v} {α : Type u_1} [topological_space β] (f : α → β) (a : α) :
theorem order_top.tendsto_at_top_nhds {β : Type v} {α : Type u_1} [partial_order α] [order_top α] [topological_space β] (f : α → β) :
@[protected, 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 α] (x : α) (F : 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 α} (h : cluster_pt x F) :
theorem filter.has_basis.cluster_pt_iff {α : Type u} {a : α} [topological_space α] {ιa : Sort u_1} {ιF : Sort u_2} {pa : ιa → Prop} {sa : ιa → set α} {pF : ιF → Prop} {sF : ιF → set α} {F : filter α} (ha : (nhds a).has_basis pa sa) (hF : F.has_basis pF sF) :
cluster_pt a F ∀ ⦃i : ιa⦄, pa i∀ ⦃j : ιF⦄, pF j(sa i sF j).nonempty
theorem cluster_pt_iff {α : Type u} [topological_space α] {x : α} {F : filter α} :
cluster_pt x F ∀ ⦃U : set α⦄, U nhds x∀ ⦃V : set α⦄, V F(U V).nonempty
theorem cluster_pt_principal_iff {α : Type u} [topological_space α] {x : α} {s : set α} :
cluster_pt x (filter.principal s) ∀ (U : set α), U nhds 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 (filter.principal s) ∃ᶠ (y : α) in nhds x, y s
theorem cluster_pt.of_le_nhds {α : Type u} [topological_space α] {x : α} {f : filter α} (H : f nhds x) [f.ne_bot] :
theorem cluster_pt.of_le_nhds' {α : Type u} [topological_space α] {x : α} {f : filter α} (H : f nhds x) (hf : f.ne_bot) :
theorem cluster_pt.of_nhds_le {α : Type u} [topological_space α] {x : α} {f : filter α} (H : nhds x f) :
theorem cluster_pt.mono {α : Type u} [topological_space α] {x : α} {f g : filter α} (H : cluster_pt x f) (h : f g) :
theorem cluster_pt.of_inf_left {α : Type u} [topological_space α] {x : α} {f g : filter α} (H : cluster_pt x (f g)) :
theorem cluster_pt.of_inf_right {α : Type u} [topological_space α] {x : α} {f g : filter α} (H : cluster_pt x (f g)) :
theorem ultrafilter.cluster_pt_iff {α : Type u} [topological_space α] {x : α} {f : ultrafilter α} :
def map_cluster_pt {α : Type u} [topological_space α] {ι : Type u_1} (x : α) (F : filter ι) (u : ι → α) :
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 nhds 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] (h : filter.tendsto φ p F) (H : filter.tendsto (u φ) p (nhds x)) :

Interior, closure and frontier in terms of neighborhoods #

theorem interior_eq_nhds' {α : Type u} [topological_space α] {s : set α} :
interior s = {a : α | s nhds a}
theorem interior_eq_nhds {α : Type u} [topological_space α] {s : set α} :
theorem mem_interior_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
@[simp]
theorem interior_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
theorem interior_set_of_eq {α : Type u} [topological_space α] {p : α → Prop} :
interior {x : α | p x} = {x : α | ∀ᶠ (y : α) in nhds x, p y}
theorem is_open_set_of_eventually_nhds {α : Type u} [topological_space α] {p : α → Prop} :
is_open {x : α | ∀ᶠ (y : α) in nhds x, p y}
theorem subset_interior_iff_nhds {α : Type u} [topological_space α] {s V : set α} :
s interior V ∀ (x : α), x sV nhds x
theorem is_open_iff_nhds {α : Type u} [topological_space α] {s : set α} :
is_open s ∀ (a : α), a snhds a filter.principal s
theorem is_open_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} :
is_open s ∀ (a : α), a ss nhds a
theorem is_open_iff_ultrafilter {α : Type u} [topological_space α] {s : set α} :
is_open s ∀ (x : α), x s∀ (l : ultrafilter α), l nhds xs l
theorem is_open_singleton_iff_nhds_eq_pure {α : Type u_1} [topological_space α] (a : α) :
theorem mem_closure_iff_frequently {α : Type u} [topological_space α] {s : set α} {a : α} :
a closure s ∃ᶠ (x : α) in nhds a, x s
theorem filter.frequently.mem_closure {α : Type u} [topological_space α] {s : set α} {a : α} :
(∃ᶠ (x : α) in nhds a, x s)a closure s

Alias of the reverse direction of mem_closure_iff_frequently.

theorem is_closed_set_of_cluster_pt {α : Type u} [topological_space α] {f : filter α} :
is_closed {x : α | cluster_pt x f}

The set of cluster points of a filter is closed. In particular, the set of limit points of a sequence is closed.

theorem mem_closure_iff_cluster_pt {α : Type u} [topological_space α] {s : set α} {a : α} :
theorem mem_closure_iff_nhds_ne_bot {α : Type u} {a : α} [topological_space α] {s : set α} :
theorem mem_closure_iff_nhds_within_ne_bot {α : Type u} [topological_space α] {s : set α} {x : α} :
theorem dense_compl_singleton {α : Type u} [topological_space α] (x : α) [(nhds_within x {x}).ne_bot] :

If x is not an isolated point of a topological space, then {x}ᶜ is dense in the whole space.

@[simp]
theorem closure_compl_singleton {α : Type u} [topological_space α] (x : α) [(nhds_within x {x}).ne_bot] :

If x is not an isolated point of a topological space, then the closure of {x}ᶜ is the whole space.

@[simp]
theorem interior_singleton {α : Type u} [topological_space α] (x : α) [(nhds_within x {x}).ne_bot] :

If x is not an isolated point of a topological space, then the interior of {x} is empty.

theorem closure_eq_cluster_pts {α : Type u} [topological_space α] {s : set α} :
theorem mem_closure_iff_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
a closure s ∀ (t : set α), t nhds a(t s).nonempty
theorem mem_closure_iff_nhds' {α : Type u} [topological_space α] {s : set α} {a : α} :
a closure s ∀ (t : set α), t nhds 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} {ι : Sort w} [topological_space α] {a : α} {p : ι → Prop} {s : ι → set α} (h : (nhds a).has_basis p s) {t : set α} :
a closure t ∀ (i : ι), p i(s i t).nonempty
theorem mem_closure_iff_nhds_basis {α : Type u} {ι : Sort w} [topological_space α] {a : α} {p : ι → Prop} {s : ι → set α} (h : (nhds 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 : ultrafilter α), s u u nhds 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 (filter.principal s)a s
theorem is_closed_iff_nhds {α : Type u} [topological_space α] {s : set α} :
is_closed s ∀ (x : α), (∀ (U : set α), U nhds x(U s).nonempty)x s
theorem closure_inter_open {α : Type u} [topological_space α] {s t : set α} (h : is_open s) :
theorem closure_inter_open' {α : Type u} [topological_space α] {s t : set α} (h : is_open t) :
theorem dense.open_subset_closure_inter {α : Type u} [topological_space α] {s t : set α} (hs : dense s) (ht : is_open t) :
t closure (t s)
theorem mem_closure_of_mem_closure_union {α : Type u} [topological_space α] {s₁ s₂ : set α} {x : α} (h : x closure (s₁ s₂)) (h₁ : s₁ nhds x) :
x closure s₂
theorem dense.inter_of_open_left {α : Type u} [topological_space α] {s t : set α} (hs : dense s) (ht : dense t) (hso : is_open s) :
dense (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 α} (hs : dense s) (ht : dense t) (hto : is_open t) :
dense (s t)

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

theorem dense.inter_nhds_nonempty {α : Type u} [topological_space α] {s t : set α} (hs : dense s) {x : α} (ht : t nhds x) :
theorem closure_diff {α : Type u} [topological_space α] {s t : set α} :
theorem filter.frequently.mem_of_closed {α : Type u} [topological_space α] {a : α} {s : set α} (h : ∃ᶠ (x : α) in nhds a, x s) (hs : is_closed s) :
a s
theorem is_closed.mem_of_frequently_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} (hs : is_closed s) (h : ∃ᶠ (x : β) in b, f x s) (hf : filter.tendsto f b (nhds a)) :
a s
theorem is_closed.mem_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} [b.ne_bot] (hs : is_closed s) (hf : filter.tendsto f b (nhds a)) (h : ∀ᶠ (x : β) in b, f x s) :
a s
theorem mem_closure_of_frequently_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} (h : ∃ᶠ (x : β) in b, f x s) (hf : filter.tendsto f b (nhds a)) :
theorem mem_closure_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} [b.ne_bot] (hf : filter.tendsto f b (nhds a)) (h : ∀ᶠ (x : β) in b, f x s) :
theorem tendsto_inf_principal_nhds_iff_of_forall_eq {α : Type u} {β : Type v} [topological_space α] {f : β → α} {l : filter β} {s : set β} {a : α} (h : ∀ (x : β), x sf x = 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 #

noncomputable def Lim {α : Type u} [topological_space α] [nonempty α] (f : filter α) :
α

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

Equations
noncomputable 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
noncomputable def ultrafilter.Lim {α : Type u} [topological_space α] :
ultrafilter α → α

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
noncomputable def lim {α : Type u} {β : Type v} [topological_space α] [nonempty α] (f : filter β) (g : β → α) :
α

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 nhds a) :
f nhds (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 (nhds a)) :
filter.tendsto g f (nhds (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.

Continuity #

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

A function between topological spaces is continuous if the preimage of every open set is open. Registered as a structure to make sure it is not unfolded by Lean.

theorem continuous_def {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ∀ (s : set β), is_open sis_open (f ⁻¹' s)
theorem is_open.preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set β} (h : is_open s) :
theorem continuous.congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} (h : continuous f) (h' : ∀ (x : α), f x = g x) :
def continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] (f : α → β) (x : α) :
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 : α} (h : continuous_at f x) :
filter.tendsto f (nhds x) (nhds (f x))
theorem continuous_at_def {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} :
continuous_at f x ∀ (A : set β), A nhds (f x)f ⁻¹' A nhds x
theorem continuous_at_congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {x : α} (h : f =ᶠ[nhds x] g) :
theorem continuous_at.congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {x : α} (hf : continuous_at f x) (h : f =ᶠ[nhds x] g) :
theorem continuous_at.preimage_mem_nhds {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {t : set β} (h : continuous_at f x) (ht : t nhds (f x)) :
theorem eventually_eq_zero_nhds {α : Type u_1} [topological_space α] {M₀ : Type u_2} [has_zero M₀] {a : α} {f : α → M₀} :
theorem cluster_pt.map {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {la : filter α} {lb : filter β} (H : cluster_pt x la) {f : α → β} (hfc : continuous_at f x) (hf : filter.tendsto f la lb) :
cluster_pt (f x) lb
theorem preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set β} (hf : continuous f) :

See also interior_preimage_subset_preimage_interior.

@[continuity]
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 : α → β} (hg : continuous g) (hf : continuous 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 : α} (hg : continuous_at g (f x)) (hf : continuous_at f x) :
theorem continuous.tendsto {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (x : α) :
filter.tendsto f (nhds x) (nhds (f x))
theorem continuous.tendsto' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (x : α) (y : β) (h : f x = y) :

A version of continuous.tendsto that allows one to specify a simpler form of the limit. E.g., one can write continuous_exp.tendsto' 0 1 exp_zero.

theorem continuous.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} (h : continuous f) :
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_at_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {b : β} :
continuous_at (λ (a : α), b) x
@[continuity]
theorem continuous_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {b : β} :
continuous (λ (a : α), b)
theorem filter.eventually_eq.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {f : α → β} {y : β} (h : f =ᶠ[nhds x] λ (_x : α), y) :
theorem continuous_of_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h : ∀ (x y : α), f x = f y) :
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 β} (h : is_closed s) :
theorem mem_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {s : set α} (hf : continuous_at f x) (hx : x closure s) :
f x closure (f '' s)
theorem continuous_at_iff_ultrafilter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} :
continuous_at f x ∀ (g : ultrafilter α), g nhds xfilter.tendsto f g (nhds (f x))
theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ∀ (x : α) (g : ultrafilter α), g nhds xfilter.tendsto f g (nhds (f x))
theorem continuous.closure_preimage_subset {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (t : set β) :
theorem continuous.frontier_preimage_subset {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (t : set β) :

Continuity and partial functions #

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

Continuity of a partial function

Equations
theorem open_dom_of_pcontinuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} (h : pcontinuous f) :
theorem pcontinuous_iff' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} :
pcontinuous f ∀ {x : α} {y : β}, y f xfilter.ptendsto' f (nhds x) (nhds y)
theorem set.maps_to.closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {t : set β} {f : α → β} (h : set.maps_to f s t) (hc : continuous f) :

If a continuous map f maps s to t, then it maps closure s to closure t.

theorem image_closure_subset_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (h : continuous f) :
f '' closure s closure (f '' s)
theorem closure_subset_preimage_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (h : continuous f) :
theorem map_mem_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {t : set β} {f : α → β} {a : α} (hf : continuous f) (ha : a closure s) (ht : ∀ (a : α), a sf a t) :
f a closure t

Function with dense range #

def dense_range {β : Type u_2} [topological_space β] {κ : Type u_5} (f : κ → β) :
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 : κ → β} (hf : function.surjective 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 : κ → β} (h : dense_range f) :
theorem dense.dense_range_coe {α : Type u_1} [topological_space α] {s : set α} (h : dense s) :
theorem continuous.range_subset_closure_image_dense {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set α} (hs : dense 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 α} (hs : dense s) :
dense (f '' s)

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

theorem dense_range.subset_closure_image_preimage_of_is_open {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} (hf : dense_range f) {s : set β} (hs : is_open s) :
s closure (f '' (f ⁻¹' s))

If f has dense range and s is an open set in the codomain of f, then the image of the preimage of s under f is dense in s.

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 β} (ht : set.maps_to f s 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 : κ → β} (hg : dense_range g) (hf : dense_range f) (cg : continuous g) :

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 : κ → β} (hf : dense_range f) :
theorem dense_range.nonempty {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} [h : nonempty β] (hf : dense_range f) :
noncomputable def dense_range.some {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} (hf : dense_range f) (b : β) :
κ

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

Equations
theorem dense_range.exists_mem_open {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} (hf : dense_range f) {s : set β} (ho : is_open s) (hs : s.nonempty) :
∃ (a : κ), f a s
theorem dense_range.mem_nhds {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} (h : dense_range f) {b : β} {U : set β} (U_in : U nhds b) :
∃ (a : κ), f a U

The library contains many lemmas stating that functions/operations are continuous. There are many ways to formulate the continuity of operations. Some are more convenient than others. Note: for the most part this note also applies to other properties (measurable, differentiable, continuous_on, ...).

The traditional way #

As an example, let's look at addition (+) : M → M → M. We can state that this is continuous in different definitionally equal ways (omitting some typing information)

However, lemmas with this conclusion are not nice to use in practice because

  1. They confuse the elaborator. The following two examples fail, because of limitations in the elaboration process.
variables {M : Type*} [has_add M] [topological_space M] [has_continuous_add M]
example : continuous (λ x : M, x + x) :=
continuous_add.comp _

example : continuous (λ x : M, x + x) :=
continuous_add.comp (continuous_id.prod_mk continuous_id)

The second is a valid proof, which is accepted if you write it as continuous_add.comp (continuous_id.prod_mk continuous_id : _)

  1. If the operation has more than 2 arguments, they are impractical to use, because in your application the arguments in the domain might be in a different order or associated differently.

The convenient way #

A much more convenient way to write continuity lemmas is like continuous.add:

continuous.add {f g : X  M} (hf : continuous f) (hg : continuous g) : continuous (λ x, f x + g x)

The conclusion can be continuous (f + g), which is definitionally equal. This has the following advantages

  • It supports projection notation, so is shorter to write.
  • continuous.add _ _ is recognized correctly by the elaborator and gives useful new goals.
  • It works generally, since the domain is a variable.

As an example for an unary operation, we have continuous.neg.

continuous.neg {f : α  G} (hf : continuous f) : continuous (λ x, -f x)

For unary functions, the elaborator is not confused when applying the traditional lemma (like continuous_neg), but it's still convenient to have the short version available (compare hf.neg.neg.neg with continuous_neg.comp $ continuous_neg.comp $ continuous_neg.comp hf).

As a harder example, consider an operation of the following type:

def strans {x : F} (γ γ' : path x x) (t₀ : I) : path x x

The precise definition is not important, only its type. The correct continuity principle for this operation is something like this:

{f : X  F} {γ γ' :  x, path (f x) (f x)} {t₀ s : X  I}
  ( : continuous γ) (hγ' : continuous γ')
  (ht : continuous t₀) (hs : continuous s) :
  continuous (λ x, strans (γ x) (γ' x) (t x) (s x))

Note that all arguments of strans are indexed over X, even the basepoint x, and the last argument s that arises since path x x has a coercion to I → F. The paths γ and γ' (which are unary functions from I) become binary functions in the continuity lemma.

Summary #

  • Make sure that your continuity lemmas are stated in the most general way, and in a convenient form. That means that:
    • The conclusion has a variable X as domain (not something like Y × Z);
    • Wherever possible, all point arguments c : Y are replaced by functions c : X → Y;
    • All n-ary function arguments are replaced by n+1-ary functions (f : Y → Z becomes f : X → Y → Z);
    • All (relevant) arguments have continuity assumptions, and perhaps there are additional assumptions needed to make the operation continuous;
    • The function in the conclusion is fully applied.
  • These remarks are mostly about the format of the conclusion of a continuity lemma. In assumptions it's fine to state that a function with more than 1 argument is continuous using or function.uncurry.

Functions with discontinuities #

In some cases, you want to work with discontinuous functions, and in certain expressions they are still continuous. For example, consider the fractional part of a number, fract : ℝ → ℝ. In this case, you want to add conditions to when a function involving fract is continuous, so you get something like this: (assumption hf could be weakened, but the important thing is the shape of the conclusion)

lemma continuous_on.comp_fract {X Y : Type*} [topological_space X] [topological_space Y]
  {f : X    Y} {g : X  } (hf : continuous f) (hg : continuous g) (h :  s, f s 0 = f s 1) :
  continuous (λ x, f x (fract (g x)))

With continuous_at you can be even more precise about what to prove in case of discontinuities, see e.g. continuous_at.comp_div_cases.