topology.basic

Basic theory of topological spaces. #

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

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 #

• `𝓝 x`: the filter `nhds x` of neighborhoods of a point `x`;
• `𝓟 s`: the principal filter of a set `s`;
• `𝓝[s] x`: the filter `nhds_within x s` of neighborhoods of a point `x` within a set `s`;
• `𝓝[≤] x`: the filter `nhds_within x (set.Iic x)` of left-neighborhoods of `x`;
• `𝓝[≥] x`: the filter `nhds_within x (set.Ici x)` of right-neighborhoods of `x`;
• `𝓝[<] x`: the filter `nhds_within x (set.Iio x)` of punctured left-neighborhoods of `x`;
• `𝓝[>] x`: the filter `nhds_within x (set.Ioi x)` of punctured right-neighborhoods of `x`;
• `𝓝[≠] x`: the filter `nhds_within x {x}ᶜ` of punctured neighborhoods of `x`.

Implementation notes #

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

Tags #

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

Topological spaces #

@[class]
structure topological_space (α : 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 T A B T) :

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

Equations
def is_open {α : Type u} (s : set α) :
Prop

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

Equations
Instances for `is_open`
theorem is_open_mk {α : Type u} {p : set α Prop} {h₁ : p set.univ} {h₂ : (s t : set α), p s p t p (s t)} {h₃ : (s : set (set α)), ( (t : set α), t s p t) p (⋃₀ s)} {s : set α} :
p s
@[ext]
theorem topological_space_eq {α : Type u} {f g : topological_space α} (h : is_open = is_open) :
f = g
@[simp]
theorem is_open_univ {α : Type u}  :
theorem is_open.inter {α : Type u} {s₁ s₂ : set α} (h₁ : is_open s₁) (h₂ : is_open s₂) :
is_open (s₁ s₂)
theorem is_open_sUnion {α : Type u} {s : set (set α)} (h : (t : set α), t s ) :
theorem topological_space_eq_iff {α : Type u} {t t' : topological_space α} :
t = t' (s : set α),
theorem is_open_fold {α : Type u} {s : set α} {t : topological_space α} :
theorem is_open_Union {α : Type u} {ι : Sort w} {f : ι set α} (h : (i : ι), is_open (f i)) :
is_open ( (i : ι), f i)
theorem is_open_bUnion {α : Type u} {β : Type v} {s : set β} {f : β set α} (h : (i : β), i s is_open (f i)) :
is_open ( (i : β) (H : i s), f i)
theorem is_open.union {α : Type u} {s₁ s₂ : set α} (h₁ : is_open s₁) (h₂ : is_open s₂) :
is_open (s₁ s₂)
@[simp]
theorem is_open_empty {α : Type u}  :
theorem is_open_sInter {α : Type u} {s : set (set α)} (hs : s.finite) :
( (t : set α), t s is_open t) is_open (⋂₀ s)
theorem is_open_bInter {α : Type u} {β : Type v} {s : set β} {f : β set α} (hs : s.finite) :
( (i : β), i s is_open (f i)) is_open ( (i : β) (H : i s), f i)
theorem is_open_Inter {α : Type u} {ι : Sort w} [finite ι] {s : ι set α} (h : (i : ι), is_open (s i)) :
is_open ( (i : ι), s i)
theorem is_open_bInter_finset {α : Type u} {β : Type v} {s : finset β} {f : β set α} (h : (i : β), i s is_open (f i)) :
is_open ( (i : β) (H : i s), f i)
theorem is_open_const {α : Type u} {p : Prop} :
is_open {a : α | p}
theorem is_open.and {α : Type u} {p₁ p₂ : α Prop}  :
is_open {a : α | p₁ a} is_open {a : α | p₂ a} is_open {a : α | p₁ a p₂ a}
@[class]
structure is_closed {α : Type u} (s : set α) :
Prop
• is_open_compl :

A set is closed if its complement is open

Instances of this typeclass
@[simp]
theorem is_open_compl_iff {α : Type u} {s : set α} :
@[simp]
theorem is_closed_empty {α : Type u}  :
@[simp]
theorem is_closed_univ {α : Type u}  :
theorem is_closed.union {α : Type u} {s₁ s₂ : set α}  :
is_closed (s₁ s₂)
theorem is_closed_sInter {α : Type u} {s : set (set α)} :
( (t : set α), t s is_closed (⋂₀ s)
theorem is_closed_Inter {α : Type u} {ι : Sort w} {f : ι set α} (h : (i : ι), is_closed (f i)) :
is_closed ( (i : ι), f i)
theorem is_closed_bInter {α : Type u} {β : Type v} {s : set β} {f : β set α} (h : (i : β), i s is_closed (f i)) :
is_closed ( (i : β) (H : i s), f i)
@[simp]
theorem is_closed_compl_iff {α : Type u} {s : set α} :
theorem is_open.is_closed_compl {α : Type u} {s : set α} (hs : is_open s) :
theorem is_open.sdiff {α : Type u} {s t : set α} (h₁ : is_open s) (h₂ : is_closed t) :
is_open (s \ t)
theorem is_closed.inter {α : Type u} {s₁ s₂ : set α} (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
is_closed (s₁ s₂)
theorem is_closed.sdiff {α : Type u} {s t : set α} (h₁ : is_closed s) (h₂ : is_open t) :
is_closed (s \ t)
theorem is_closed_bUnion {α : Type u} {β : Type v} {s : set β} {f : β set α} (hs : s.finite) :
( (i : β), i s is_closed (f i)) is_closed ( (i : β) (H : i s), f i)
theorem is_closed_Union {α : Type u} {ι : Sort w} [finite ι] {s : ι set α} (h : (i : ι), is_closed (s i)) :
is_closed ( (i : ι), s i)
theorem is_closed_imp {α : Type u} {p q : α Prop} (hp : is_open {x : α | p x}) (hq : is_closed {x : α | q x}) :
is_closed {x : α | p x q x}
theorem is_closed.not {α : Type u} {p : α Prop}  :
is_closed {a : α | p a} is_open {a : α | ¬p a}

Interior of a set #

def interior {α : Type u} (s : set α) :
set α

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

Equations
theorem mem_interior {α : Type u} {s : set α} {x : α} :
x (t : set α) (H : t s), x t
@[simp]
theorem is_open_interior {α : Type u} {s : set α} :
theorem interior_subset {α : Type u} {s : set α} :
s
theorem interior_maximal {α : Type u} {s t : set α} (h₁ : t s) (h₂ : is_open t) :
t
theorem is_open.interior_eq {α : Type u} {s : set α} (h : is_open s) :
= s
theorem interior_eq_iff_is_open {α : Type u} {s : set α} :
= s
theorem subset_interior_iff_is_open {α : Type u} {s : set α} :
s
theorem is_open.subset_interior_iff {α : Type u} {s t : set α} (h₁ : is_open s) :
s s t
theorem subset_interior_iff {α : Type u} {s t : set α} :
t (U : set α), t U U s
theorem interior_mono {α : Type u} {s t : set α} (h : s t) :
@[simp]
theorem interior_empty {α : Type u}  :
@[simp]
theorem interior_univ {α : Type u}  :
@[simp]
theorem interior_eq_univ {α : Type u} {s : set α} :
@[simp]
theorem interior_interior {α : Type u} {s : set α} :
@[simp]
theorem interior_inter {α : Type u} {s t : set α} :
interior (s t) =
@[simp]
theorem finset.interior_Inter {α : Type u} {ι : 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} {ι : Type u_1} [finite ι] (f : ι set α) :
interior ( (i : ι), f i) = (i : ι), interior (f i)
theorem interior_union_is_closed_of_interior_empty {α : Type u} {s t : set α} (h₁ : is_closed s) (h₂ : = ) :
interior (s t) =
theorem is_open_iff_forall_mem_open {α : Type u} {s : set α}  :
(x : α), x s ( (t : set α) (H : t s), x t)
theorem interior_Inter_subset {α : Type u} {ι : Sort w} (s : ι set α) :
interior ( (i : ι), s i) (i : ι), interior (s i)
theorem interior_Inter₂_subset {α : Type u} {ι : Sort w} (p : ι Sort u_1) (s : Π (i : ι), p i set α) :
interior ( (i : ι) (j : p i), s i j) (i : ι) (j : p i), interior (s i j)
theorem interior_sInter_subset {α : Type u} (S : set (set α)) :
interior (⋂₀ S) (s : set α) (H : s S),

Closure of a set #

def closure {α : Type u} (s : set α) :
set α

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

Equations
@[simp]
theorem is_closed_closure {α : Type u} {s : set α} :
theorem subset_closure {α : Type u} {s : set α} :
s
theorem not_mem_of_not_mem_closure {α : Type u} {s : set α} {P : α} (hP : P ) :
P s
theorem closure_minimal {α : Type u} {s t : set α} (h₁ : s t) (h₂ : is_closed t) :
t
theorem disjoint.closure_left {α : Type u} {s t : set α} (hd : t) (ht : is_open t) :
theorem disjoint.closure_right {α : Type u} {s t : set α} (hd : t) (hs : is_open s) :
(closure t)
theorem is_closed.closure_eq {α : Type u} {s : set α} (h : is_closed s) :
= s
theorem is_closed.closure_subset {α : Type u} {s : set α} (hs : is_closed s) :
s
theorem is_closed.closure_subset_iff {α : Type u} {s t : set α} (h₁ : is_closed t) :
t s t
theorem is_closed.mem_iff_closure_subset {α : Type u} {s : set α} (hs : is_closed s) {x : α} :
x s closure {x} s
theorem closure_mono {α : Type u} {s t : set α} (h : s t) :
theorem monotone_closure (α : Type u_1)  :
theorem diff_subset_closure_iff {α : Type u} {s t : set α} :
s \ t s
theorem closure_inter_subset_inter_closure {α : Type u} (s t : set α) :
theorem is_closed_of_closure_subset {α : Type u} {s : set α} (h : s) :
theorem closure_eq_iff_is_closed {α : Type u} {s : set α} :
= s
theorem closure_subset_iff_is_closed {α : Type u} {s : set α} :
s
@[simp]
theorem closure_empty {α : Type u}  :
@[simp]
theorem closure_empty_iff {α : Type u} (s : set α) :
s =
@[simp]
theorem closure_nonempty_iff {α : Type u} {s : set α} :
theorem set.nonempty.of_closure {α : Type u} {s : set α} :

Alias of the forward direction of `closure_nonempty_iff`.

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

Alias of the reverse direction of `closure_nonempty_iff`.

@[simp]
theorem closure_univ {α : Type u}  :
@[simp]
theorem closure_closure {α : Type u} {s : set α} :
@[simp]
theorem closure_union {α : Type u} {s t : set α} :
closure (s t) =
@[simp]
theorem finset.closure_bUnion {α : Type u} {ι : 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} {ι : Type u_1} [finite ι] (f : ι set α) :
closure ( (i : ι), f i) = (i : ι), closure (f i)
theorem interior_subset_closure {α : Type u} {s : set α} :
theorem closure_eq_compl_interior_compl {α : Type u} {s : set α} :
@[simp]
theorem interior_compl {α : Type u} {s : set α} :
@[simp]
theorem closure_compl {α : Type u} {s : set α} :
theorem mem_closure_iff {α : Type u} {s : set α} {a : α} :
a (o : set α), a o (o s).nonempty
theorem closure_inter_open_nonempty_iff {α : Type u} {s t : set α} (h : is_open t) :
theorem filter.le_lift'_closure {α : Type u} (l : filter α) :
l
theorem filter.has_basis.lift'_closure {α : Type u} {ι : Sort w} {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} {l : filter α} {p : ι Prop} {s : ι set α} (h : l.has_basis p s) (hc : (i : ι), p i is_closed (s i)) :
= l
@[simp]
theorem filter.lift'_closure_eq_bot {α : Type u} {l : filter α} :
l =
def dense {α : Type u} (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} {s : set α} :
theorem dense.closure_eq {α : Type u} {s : set α} (h : dense s) :
theorem interior_eq_empty_iff_dense_compl {α : Type u} {s : set α} :
theorem dense.interior_compl {α : Type u} {s : set α} (h : dense s) :
@[simp]
theorem dense_closure {α : Type u} {s : set α} :

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

theorem dense.of_closure {α : Type u} {s : set α} :

Alias of the forward direction of `dense_closure`.

theorem dense.closure {α : Type u} {s : set α} :

Alias of the reverse direction of `dense_closure`.

@[simp]
theorem dense_univ {α : Type u}  :
theorem dense_iff_inter_open {α : Type u} {s : set α} :
(U : set α), U.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} {s : set α} :
(U : set α), U.nonempty (U s).nonempty

Alias of the forward direction of `dense_iff_inter_open`.

theorem dense.exists_mem_open {α : Type u} {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} {s : set α} (hs : dense s) :
theorem dense.nonempty {α : Type u} [h : nonempty α] {s : set α} (hs : dense s) :
theorem dense.mono {α : Type u} {s₁ s₂ : set α} (h : s₁ s₂) (hd : dense s₁) :
dense s₂
theorem dense_compl_singleton_iff_not_open {α : Type u} {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} (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} (s : set α) :
\ =
@[simp]
theorem closure_diff_frontier {α : Type u} (s : set α) :
\ =
@[simp]
theorem self_diff_frontier {α : Type u} (s : set α) :
s \ =
theorem frontier_eq_closure_inter_closure {α : Type u} {s : set α} :
=
theorem frontier_subset_closure {α : Type u} {s : set α} :
theorem is_closed.frontier_subset {α : Type u} {s : set α} (hs : is_closed s) :
s
theorem frontier_closure_subset {α : Type u} {s : set α} :
theorem frontier_interior_subset {α : Type u} {s : set α} :
@[simp]
theorem frontier_compl {α : Type u} (s : set α) :

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

@[simp]
theorem frontier_univ {α : Type u}  :
@[simp]
theorem frontier_empty {α : Type u}  :
theorem frontier_inter_subset {α : Type u} (s t : set α) :
theorem frontier_union_subset {α : Type u} (s t : set α) :
theorem is_closed.frontier_eq {α : Type u} {s : set α} (hs : is_closed s) :
= s \
theorem is_open.frontier_eq {α : Type u} {s : set α} (hs : is_open s) :
= \ s
theorem is_open.inter_frontier_eq {α : Type u} {s : set α} (hs : is_open s) :
theorem is_closed_frontier {α : Type u} {s : set α} :

The frontier of a set is closed.

theorem interior_frontier {α : Type u} {s : set α} (h : is_closed s) :

The frontier of a closed set has no interior point.

theorem closure_eq_interior_union_frontier {α : Type u} (s : set α) :
=
theorem closure_eq_self_union_frontier {α : Type u} (s : set α) :
= s
theorem disjoint.frontier_left {α : Type u} {s t : set α} (ht : is_open t) (hd : t) :
theorem disjoint.frontier_right {α : Type u} {s t : set α} (hs : is_open s) (hd : t) :
theorem compl_frontier_eq_union_interior {α : Type u} {s : set α} :

Neighborhoods #

@[irreducible]
def nhds {α : Type u} (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`
def nhds_within {α : Type u} (a : α) (s : set α) :

The "neighborhood within" filter. Elements of `𝓝[s] a` are sets containing the intersection of `s` and a neighborhood of `a`.

Equations
• s =
Instances for `nhds_within`
theorem nhds_def {α : Type u} (a : α) :
nhds a = (s : set α) (H : s {s : set α | a s is_open s}),
theorem nhds_def' {α : Type u} (a : α) :
nhds a = (s : set α) (hs : is_open s) (ha : a s),
theorem nhds_basis_opens {α : Type u} (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} (a : α) :
(nhds a).has_basis (λ (s : set α), a s has_compl.compl
theorem le_nhds_iff {α : Type u} {f : filter α} {a : α} :
f nhds a (s : set α), a s s 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} {f : filter α} {a : α} {s : set α} (h : a s) (o : is_open s) (sf : 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} {a : α} {s : set α} :
s nhds a (t : set α) (H : t s), a t
theorem eventually_nhds_iff {α : Type u} {a : α} {p : α Prop} :
(∀ᶠ (x : α) in nhds a, p x) (t : set α), ( (x : α), x t p x) 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} {a : α} {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} {a : α} {s : set α} :
s nhds a a s
theorem filter.eventually.self_of_nhds {α : Type u} {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} {a : α} {s : set α} (hs : is_open s) (ha : a s) :
s nhds a
theorem is_open.mem_nhds_iff {α : Type u} {a : α} {s : set α} (hs : is_open s) :
s nhds a a s
theorem is_closed.compl_mem_nhds {α : Type u} {a : α} {s : set α} (hs : is_closed s) (ha : a s) :
theorem is_open.eventually_mem {α : Type u} {a : α} {s : set α} (hs : is_open s) (ha : a s) :
∀ᶠ (x : α) in nhds a, x s
theorem nhds_basis_opens' {α : Type u} (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} {s U : set α} (h : (x : α), x s U nhds x) :
(V : set α), s 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} {s U : set α} (h : U (x : α) (H : x s), nhds x) :
(V : set α), s 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} {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} {p : α Prop} {a : α} :
(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhds y, p x) ∀ᶠ (x : α) in nhds a, p x
@[simp]
theorem frequently_frequently_nhds {α : Type u} {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} {s : set α} {a : α} :
(∀ᶠ (x : α) in nhds a, s nhds x) s nhds a
@[simp]
theorem nhds_bind_nhds {α : Type u} {a : α}  :
@[simp]
theorem eventually_eventually_eq_nhds {α : Type u} {β : Type v} {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} {f g : α β} {a : α} (h : f =ᶠ[nhds a] g) :
f a = g a
@[simp]
theorem eventually_eventually_le_nhds {α : Type u} {β : Type v} [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} {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} [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} (x : α) (P : set α Prop) (hP : (s t : set α), s t P s P t) :
( (s : set α), s nhds x P s) (s : set α), x s P s
theorem all_mem_nhds_filter {α : Type u} {β : Type v} (x : α) (f : set α set β) (hf : (s t : set α), s t f s f t) (l : filter β) :
( (s : set α), s nhds x f s l) (s : set α), x s f s l
theorem tendsto_nhds {α : Type u} {β : Type v} {f : β α} {l : filter β} {a : α} :
(nhds a) (s : set α), a s f ⁻¹' s l
theorem tendsto_at_top_nhds {α : Type u} {β : Type v} [nonempty β] {f : β α} {a : α} :
(U : set α), a U ( (N : β), (n : β), N n f n U)
theorem tendsto_const_nhds {α : Type u} {β : Type v} {a : α} {f : filter β} :
filter.tendsto (λ (b : β), a) f (nhds a)
theorem tendsto_at_top_of_eventually_const {α : Type u} {ι : Type u_1} [nonempty ι] {x : α} {u : ι α} {i₀ : ι} (h : (i : ι), i i₀ u i = x) :
theorem tendsto_at_bot_of_eventually_const {α : Type u} {ι : Type u_1} [nonempty ι] {x : α} {u : ι α} {i₀ : ι} (h : (i : ι), i i₀ u i = x) :
theorem pure_le_nhds {α : Type u}  :
theorem tendsto_pure_nhds {β : Type v} {α : Type u_1} (f : α β) (a : α) :
(nhds (f a))
theorem order_top.tendsto_at_top_nhds {β : Type v} {α : Type u_1} [order_top α] (f : α β) :
(nhds (f ))
@[protected, simp, instance]
def nhds_ne_bot {α : Type u} {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} (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, but beware that terminology varies. This is not the same as asking `𝓝[≠] x ⊓ F ≠ ⊥`. See `mem_closure_iff_cluster_pt` in particular.

Equations
theorem cluster_pt.ne_bot {α : Type u} {x : α} {F : filter α} (h : F) :
theorem filter.has_basis.cluster_pt_iff {α : Type u} {a : α} {ι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) :
F ⦃i : ιa⦄, pa i ⦃j : ιF⦄, pF j (sa i sF j).nonempty
theorem cluster_pt_iff {α : Type u} {x : α} {F : filter α} :
F ⦃U : set α⦄, U nhds x ⦃V : set α⦄, V F (U V).nonempty
theorem cluster_pt_principal_iff {α : Type u} {x : α} {s : set α} :
(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. See also `mem_closure_iff_cluster_pt`.

theorem cluster_pt_principal_iff_frequently {α : Type u} {x : α} {s : set α} :
∃ᶠ (y : α) in nhds x, y s
theorem cluster_pt.of_le_nhds {α : Type u} {x : α} {f : filter α} (H : f nhds x) [f.ne_bot] :
f
theorem cluster_pt.of_le_nhds' {α : Type u} {x : α} {f : filter α} (H : f nhds x) (hf : f.ne_bot) :
f
theorem cluster_pt.of_nhds_le {α : Type u} {x : α} {f : filter α} (H : nhds x f) :
f
theorem cluster_pt.mono {α : Type u} {x : α} {f g : filter α} (H : f) (h : f g) :
g
theorem cluster_pt.of_inf_left {α : Type u} {x : α} {f g : filter α} (H : (f g)) :
f
theorem cluster_pt.of_inf_right {α : Type u} {x : α} {f g : filter α} (H : (f g)) :
g
theorem ultrafilter.cluster_pt_iff {α : Type u} {x : α} {f : ultrafilter α} :
def map_cluster_pt {α : Type u} {ι : 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
• u = F)
theorem map_cluster_pt_iff {α : Type u} {ι : Type u_1} (x : α) (F : filter ι) (u : ι α) :
u (s : set α), s nhds x (∃ᶠ (a : ι) in F, u a s)
theorem map_cluster_pt_of_comp {α : Type u} {ι : Type u_1} {δ : Type u_2} {F : filter ι} {φ : δ ι} {p : filter δ} {x : α} {u : ι α} [p.ne_bot] (h : F) (H : filter.tendsto (u φ) p (nhds x)) :
u
def acc_pt {α : Type u} (x : α) (F : filter α) :
Prop

A point `x` is an accumulation point of a filter `F` if `𝓝[≠] x ⊓ F ≠ ⊥`.

Equations
theorem acc_iff_cluster {α : Type u} (x : α) (F : filter α) :
F F)
theorem acc_principal_iff_cluster {α : Type u} (x : α) (C : set α) :

`x` is an accumulation point of a set `C` iff it is a cluster point of `C ∖ {x}`.

theorem acc_pt_iff_nhds {α : Type u} (x : α) (C : set α) :
(U : set α), U nhds x ( (y : α) (H : y U C), y x)

`x` is an accumulation point of a set `C` iff every neighborhood of `x` contains a point of `C` other than `x`.

theorem acc_pt_iff_frequently {α : Type u} (x : α) (C : set α) :
∃ᶠ (y : α) in nhds x, y x y C

`x` is an accumulation point of a set `C` iff there are points near `x` in `C` and different from `x`.

theorem acc_pt.mono {α : Type u} {x : α} {F G : filter α} (h : F) (hFG : F G) :
G

If `x` is an accumulation point of `F` and `F ≤ G`, then `x` is an accumulation point of `D.

Interior, closure and frontier in terms of neighborhoods #

theorem interior_eq_nhds' {α : Type u} {s : set α} :
= {a : α | s nhds a}
theorem interior_eq_nhds {α : Type u} {s : set α} :
= {a : α |
theorem mem_interior_iff_mem_nhds {α : Type u} {s : set α} {a : α} :
a s nhds a
@[simp]
theorem interior_mem_nhds {α : Type u} {s : set α} {a : α} :
theorem interior_set_of_eq {α : Type u} {p : α Prop} :
interior {x : α | p x} = {x : α | ∀ᶠ (y : α) in nhds x, p y}
theorem is_open_set_of_eventually_nhds {α : Type u} {p : α Prop} :
is_open {x : α | ∀ᶠ (y : α) in nhds x, p y}
theorem subset_interior_iff_nhds {α : Type u} {s V : set α} :
s (x : α), x s V nhds x
theorem is_open_iff_nhds {α : Type u} {s : set α} :
(a : α), a s
theorem is_open_iff_mem_nhds {α : Type u} {s : set α} :
(a : α), a s s nhds a
theorem is_open_iff_eventually {α : Type u} {s : set α} :
(x : α), x s (∀ᶠ (y : α) in nhds x, y s)

A set `s` is open iff for every point `x` in `s` and every `y` close to `x`, `y` is in `s`.

theorem is_open_iff_ultrafilter {α : Type u} {s : set α} :
(x : α), x s (l : , l nhds x s l
theorem is_open_singleton_iff_nhds_eq_pure {α : Type u} (a : α) :
theorem is_open_singleton_iff_punctured_nhds {α : Type u_1} (a : α) :
theorem mem_closure_iff_frequently {α : Type u} {s : set α} {a : α} :
a ∃ᶠ (x : α) in nhds a, x s
theorem filter.frequently.mem_closure {α : Type u} {s : set α} {a : α} :
(∃ᶠ (x : α) in nhds a, x s) a

Alias of the reverse direction of `mem_closure_iff_frequently`.

theorem is_closed_iff_frequently {α : Type u} {s : set α} :
(x : α), (∃ᶠ (y : α) in nhds x, y s) x s

A set `s` is closed iff for every point `x`, if there is a point `y` close to `x` that belongs to `s` then `x` is in `s`.

theorem is_closed_set_of_cluster_pt {α : Type u} {f : filter α} :
is_closed {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} {s : set α} {a : α} :
a
theorem mem_closure_iff_nhds_ne_bot {α : Type u} {a : α} {s : set α} :
theorem mem_closure_iff_nhds_within_ne_bot {α : Type u} {s : set α} {x : α} :
theorem dense_compl_singleton {α : Type u} (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} (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} (x : α) [ {x}).ne_bot] :

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

theorem not_is_open_singleton {α : Type u} (x : α) [ {x}).ne_bot] :
theorem closure_eq_cluster_pts {α : Type u} {s : set α} :
= {a : α | (filter.principal s)}
theorem mem_closure_iff_nhds {α : Type u} {s : set α} {a : α} :
a (t : set α), t nhds a (t s).nonempty
theorem mem_closure_iff_nhds' {α : Type u} {s : set α} {a : α} :
a (t : set α), t nhds a ( (y : s), y t)
theorem mem_closure_iff_comap_ne_bot {α : Type u} {A : set α} {x : α} :
theorem mem_closure_iff_nhds_basis' {α : Type u} {ι : Sort w} {a : α} {p : ι Prop} {s : ι set α} (h : (nhds a).has_basis p s) {t : set α} :
a (i : ι), p i (s i t).nonempty
theorem mem_closure_iff_nhds_basis {α : Type u} {ι : Sort w} {a : α} {p : ι Prop} {s : ι set α} (h : (nhds a).has_basis p s) {t : set α} :
a (i : ι), p i ( (y : α) (H : y t), y s i)
theorem mem_closure_iff_ultrafilter {α : Type u} {s : set α} {x : α} :
x (u : , 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} {s : set α} :
(a : α), a s
theorem is_closed_iff_nhds {α : Type u} {s : set α} :
(x : α), ( (U : set α), U nhds x (U s).nonempty) x s
theorem is_closed.interior_union_left {α : Type u} {s t : set α} (h : is_closed s) :
interior (s t) s
theorem is_closed.interior_union_right {α : Type u} {s t : set α} (h : is_closed t) :
theorem is_open.inter_closure {α : Type u} {s t : set α} (h : is_open s) :
s closure (s t)
theorem is_open.closure_inter {α : Type u} {s t : set α} (h : is_open t) :
t closure (s t)
theorem dense.open_subset_closure_inter {α : Type u} {s t : set α} (hs : dense s) (ht : is_open t) :
t closure (t s)
theorem mem_closure_of_mem_closure_union {α : Type u} {s₁ s₂ : set α} {x : α} (h : x closure (s₁ s₂)) (h₁ : s₁ nhds x) :
x closure s₂
theorem dense.inter_of_open_left {α : Type u} {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} {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} {s t : set α} (hs : dense s) {x : α} (ht : t nhds x) :
theorem closure_diff {α : Type u} {s t : set α} :
\ closure (s \ t)
theorem filter.frequently.mem_of_closed {α : Type u} {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} {f : β α} {b : filter β} {a : α} {s : set α} (hs : is_closed s) (h : ∃ᶠ (x : β) in b, f x s) (hf : (nhds a)) :
a s
theorem is_closed.mem_of_tendsto {α : Type u} {β : Type v} {f : β α} {b : filter β} {a : α} {s : set α} [b.ne_bot] (hs : is_closed s) (hf : (nhds a)) (h : ∀ᶠ (x : β) in b, f x s) :
a s
theorem mem_closure_of_frequently_of_tendsto {α : Type u} {β : Type v} {f : β α} {b : filter β} {a : α} {s : set α} (h : ∃ᶠ (x : β) in b, f x s) (hf : (nhds a)) :
a
theorem mem_closure_of_tendsto {α : Type u} {β : Type v} {f : β α} {b : filter β} {a : α} {s : set α} [b.ne_bot] (hf : (nhds a)) (h : ∀ᶠ (x : β) in b, f x s) :
a
theorem tendsto_inf_principal_nhds_iff_of_forall_eq {α : Type u} {β : Type v} {f : β α} {l : filter β} {s : set β} {a : α} (h : (x : β), x s f x = a) :
(l (nhds a) (nhds 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} [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} (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}  :
α

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

See also `interior_preimage_subset_preimage_interior`.

@[continuity]
theorem continuous_id {α : Type u_1}  :
theorem continuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} (hg : continuous g) (hf : continuous f) :
theorem continuous.iterate {α : Type u_1} {f : α α} (h : continuous f) (n : ) :
theorem continuous_at.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} {x : α} (hg : (f x)) (hf : x) :
theorem continuous_at.comp_of_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β γ} {f : α β} {x : α} {y : β} (hg : y) (hf : x) (hy : f x = y) :
theorem continuous.tendsto {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) (x : α) :
(nhds x) (nhds (f x))
theorem continuous.tendsto' {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) (x : α) (y : β) (h : f x = y) :
(nhds x) (nhds 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} {f : α β} {x : α} (h : continuous f) :
theorem continuous_iff_continuous_at {α : Type u_1} {β : Type u_2} {f : α β} :
(x : α),
theorem continuous_at_const {α : Type u_1} {β : Type u_2} {x : α} {b : β} :
continuous_at (λ (a : α), b) x
@[continuity]
theorem continuous_const {α : Type u_1} {β : Type u_2} {b : β} :
continuous (λ (a : α), b)
theorem filter.eventually_eq.continuous_at {α : Type u_1} {β : Type u_2} {x : α} {f : α β} {y : β} (h : f =ᶠ[nhds x] λ (_x : α), y) :
theorem continuous_of_const {α : Type u_1} {β : Type u_2} {f : α β} (h : (x y : α), f x = f y) :
theorem continuous_at_id {α : Type u_1} {x : α} :
theorem continuous_at.iterate {α : Type u_1} {f : α α} {x : α} (hf : x) (hx : f x = x) (n : ) :
x
theorem continuous_iff_is_closed {α : Type u_1} {β : Type u_2} {f : α β} :
(s : set β), is_closed (f ⁻¹' s)
theorem is_closed.preimage {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) {s : set β} (h : is_closed s) :
theorem mem_closure_image {α : Type u_1} {β : Type u_2} {f : α β} {x : α} {s : set α} (hf : x) (hx : x ) :
f x closure (f '' s)
theorem continuous_at_iff_ultrafilter {α : Type u_1} {β : Type u_2} {f : α β} {x : α} :
(g : , g nhds x (nhds (f x))
theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} {f : α β} :
(x : α) (g : , g nhds x (nhds (f x))
theorem continuous.closure_preimage_subset {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) (t : set β) :
theorem continuous.frontier_preimage_subset {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) (t : set β) :
theorem set.maps_to.closure {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {f : α β} (h : s t) (hc : continuous f) :
(closure s) (closure t)

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} {f : α β} {s : set α} (h : continuous f) :
f '' closure (f '' s)
theorem closure_subset_preimage_closure_image {α : Type u_1} {β : Type u_2} {f : α β} {s : set α} (h : continuous f) :
f ⁻¹' closure (f '' s)
theorem map_mem_closure {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {f : α β} {a : α} (hf : continuous f) (ha : a ) (ht : s t) :
f a
theorem set.maps_to.closure_left {α : Type u_1} {β : Type u_2} {s : set α} {t : set β} {f : α β} (h : s t) (hc : continuous f) (ht : is_closed t) :
(closure s) t

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

Function with dense range #

def dense_range {β : Type u_2} {κ : 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} {κ : Type u_5} {f : κ β} (hf : function.surjective f) :

A surjective map has dense range.

theorem dense_range_id {α : Type u_1}  :
theorem dense_range_iff_closure_range {β : Type u_2} {κ : Type u_5} {f : κ β} :
theorem dense_range.closure_range {β : Type u_2} {κ : Type u_5} {f : κ β} (h : dense_range f) :
theorem dense.dense_range_coe {α : Type u_1} {s : set α} (h : dense s) :
theorem continuous.range_subset_closure_image_dense {α : Type u_1} {β : Type u_2} {f : α β} (hf : continuous f) {s : set α} (hs : dense s) :
closure (f '' s)
theorem dense_range.dense_image {α : Type u_1} {β : Type u_2} {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} {κ : 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} {f : α β} (hf' : dense_range f) (hf : continuous f) {s : set α} (hs : dense s) {t : set β} (ht : 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} {κ : 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} {κ : Type u_5} {f : κ β} (hf : dense_range f) :
theorem dense_range.nonempty {β : Type u_2} {κ : Type u_5} {f : κ β} [h : nonempty β] (hf : dense_range f) :
noncomputable def dense_range.some {β : Type u_2} {κ : 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} {κ : 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} {κ : 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)

• `continuous (λ p, p.1 + p.2)`;
• `continuous (function.uncurry (+))`;
• `continuous ↿(+)`. (`↿` is notation for recursively uncurrying a function)

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) :=

example : continuous (λ x : M, x + x) :=
``````

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}
(hγ : 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`.

Lean's elaborator has trouble elaborating applications of lemmas that state that the composition of two functions satisfy some property at a point, like `continuous_at.comp` / `cont_diff_at.comp` and `cont_mdiff_within_at.comp`. The reason is that a lemma like this looks like `continuous_at g (f x) → continuous_at f x → continuous_at (g ∘ f) x`. Since Lean's elaborator elaborates the arguments from left-to-right, when you write `hg.comp hf`, the elaborator will try to figure out both `f` and `g` from the type of `hg`. It tries to figure out `f` just from the point where `g` is continuous. For example, if `hg : continuous_at g (a, x)` then the elaborator will assign `f` to the function `prod.mk a`, since in that case `f x = (a, x)`. This is undesirable in most cases where `f` is not a variable. There are some ways to work around this, for example by giving `f` explicitly, or to force Lean to elaborate `hf` before elaborating `hg`, but this is annoying. Another better solution is to reformulate composition lemmas to have the following shape `continuous_at g y → continuous_at f x → f x = y → continuous_at (g ∘ f) x`. This is even useful if the proof of `f x = y` is `rfl`. The reason that this works better is because the type of `hg` doesn't mention `f`. Only after elaborating the two `continuous_at` arguments, Lean will try to unify `f x` with `y`, which is often easy after having chosen the correct functions for `f` and `g`. Here is an example that shows the difference:

``````example {x₀ : α} (f : α → α → β) (hf : continuous_at (function.uncurry f) (x₀, x₀)) :
continuous_at (λ x => f x x) x₀ :=
-- hf.comp x (continuous_at_id.prod continuous_at_id) -- type mismatch
-- hf.comp_of_eq (continuous_at_id.prod continuous_at_id) rfl -- works
``````