mathlib3 documentation

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 #

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 #

source
@[class]
structure topological_space (α : Type u) :
Type u

A topology on α.

Instances of this typeclass
Instances of other typeclasses for topological_space
source
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) :
topological_space α

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

Equations
source
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
Instances for is_open
source
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 α} :
is_open s ↔ p s
source
@[ext]
theorem topological_space_eq {α : Type u} {f g : topological_space α} (h : is_open = is_open) :
f = g
source
@[simp]
theorem is_open_univ {α : Type u} [topological_space α] :
is_open set.univ
source
theorem is_open.inter {α : Type u} {s₁ s₂ : set α} [topological_space α] (h₁ : is_open s₁) (h₂ : is_open s₂) :
is_open (s₁ ∩ s₂)
source
theorem is_open_sUnion {α : Type u} [topological_space α] {s : set (set α)} (h : ∀ (t : set α), t ∈ s → is_open t) :
is_open (⋃₀ s)
source
theorem topological_space_eq_iff {α : Type u} {t t' : topological_space α} :
t = t' ↔ ∀ (s : set α), is_open s ↔ is_open s
source
theorem is_open_fold {α : Type u} {s : set α} {t : topological_space α} :
topological_space.is_open s = is_open s
source
theorem is_open_Union {α : Type u} {ι : Sort w} [topological_space α] {f : ι → set α} (h : ∀ (i : ι), is_open (f i)) :
is_open (⋃ (i : ι), f i)
source
theorem is_open_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (h : ∀ (i : β), i ∈ s → is_open (f i)) :
is_open (⋃ (i : β) (H : i ∈ s), f i)
source
theorem is_open.union {α : Type u} {s₁ s₂ : set α} [topological_space α] (h₁ : is_open s₁) (h₂ : is_open s₂) :
is_open (s₁ ∪ s₂)
source
@[simp]
theorem is_open_empty {α : Type u} [topological_space α] :
is_open ∅
source
theorem is_open_sInter {α : Type u} [topological_space α] {s : set (set α)} (hs : s.finite) :
(∀ (t : set α), t ∈ s → is_open t) → is_open (⋂₀ s)
source
theorem is_open_bInter {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (hs : s.finite) :
(∀ (i : β), i ∈ s → is_open (f i)) → is_open (⋂ (i : β) (H : i ∈ s), f i)
source
theorem is_open_Inter {α : Type u} {ι : Sort w} [topological_space α] [finite ι] {s : ι → set α} (h : ∀ (i : ι), is_open (s i)) :
is_open (⋂ (i : ι), s i)
source
theorem is_open_bInter_finset {α : Type u} {β : Type v} [topological_space α] {s : finset β} {f : β → set α} (h : ∀ (i : β), i ∈ s → is_open (f i)) :
is_open (⋂ (i : β) (H : i ∈ s), f i)
source
theorem is_open_const {α : Type u} [topological_space α] {p : Prop} :
is_open {a : α | p}
source
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}
source
@[class]
structure is_closed {α : Type u} [topological_space α] (s : set α) :
Prop

A set is closed if its complement is open

Instances of this typeclass
source
@[simp]
theorem is_open_compl_iff {α : Type u} [topological_space α] {s : set α} :
is_open sᶜ ↔ is_closed s
source
@[simp]
theorem is_closed_empty {α : Type u} [topological_space α] :
is_closed ∅
source
@[simp]
theorem is_closed_univ {α : Type u} [topological_space α] :
is_closed set.univ
source
theorem is_closed.union {α : Type u} {s₁ s₂ : set α} [topological_space α] :
is_closed s₁ → is_closed s₂ → is_closed (s₁ ∪ s₂)
source
theorem is_closed_sInter {α : Type u} [topological_space α] {s : set (set α)} :
(∀ (t : set α), t ∈ s → is_closed t) → is_closed (⋂₀ s)
source
theorem is_closed_Inter {α : Type u} {ι : Sort w} [topological_space α] {f : ι → set α} (h : ∀ (i : ι), is_closed (f i)) :
is_closed (⋂ (i : ι), f i)
source
theorem is_closed_bInter {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (h : ∀ (i : β), i ∈ s → is_closed (f i)) :
is_closed (⋂ (i : β) (H : i ∈ s), f i)
source
@[simp]
theorem is_closed_compl_iff {α : Type u} [topological_space α] {s : set α} :
is_closed sᶜ ↔ is_open s
source
theorem is_open.is_closed_compl {α : Type u} [topological_space α] {s : set α} (hs : is_open s) :
is_closed sᶜ
source
theorem is_open.sdiff {α : Type u} [topological_space α] {s t : set α} (h₁ : is_open s) (h₂ : is_closed t) :
is_open (s \ t)
source
theorem is_closed.inter {α : Type u} {s₁ s₂ : set α} [topological_space α] (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
is_closed (s₁ ∩ s₂)
source
theorem is_closed.sdiff {α : Type u} [topological_space α] {s t : set α} (h₁ : is_closed s) (h₂ : is_open t) :
is_closed (s \ t)
source
theorem is_closed_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} (hs : s.finite) :
(∀ (i : β), i ∈ s → is_closed (f i)) → is_closed (⋃ (i : β) (H : i ∈ s), f i)
source
theorem is_closed_Union {α : Type u} {ι : Sort w} [topological_space α] [finite ι] {s : ι → set α} (h : ∀ (i : ι), is_closed (s i)) :
is_closed (⋃ (i : ι), s i)
source
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 x → q x}
source
theorem is_closed.not {α : Type u} {p : α → Prop} [topological_space α] :
is_closed {a : α | p a} → is_open {a : α | ¬p a}

Interior of a set #

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

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

Equations
source
theorem mem_interior {α : Type u} [topological_space α] {s : set α} {x : α} :
x ∈ interior s ↔ ∃ (t : set α) (H : t ⊆ s), is_open t ∧ x ∈ t
source
@[simp]
theorem is_open_interior {α : Type u} [topological_space α] {s : set α} :
is_open (interior s)
source
theorem interior_subset {α : Type u} [topological_space α] {s : set α} :
interior s ⊆ s
source
theorem interior_maximal {α : Type u} [topological_space α] {s t : set α} (h₁ : t ⊆ s) (h₂ : is_open t) :
t ⊆ interior s
source
theorem is_open.interior_eq {α : Type u} [topological_space α] {s : set α} (h : is_open s) :
interior s = s
source
theorem interior_eq_iff_is_open {α : Type u} [topological_space α] {s : set α} :
interior s = s ↔ is_open s
source
theorem subset_interior_iff_is_open {α : Type u} [topological_space α] {s : set α} :
s ⊆ interior s ↔ is_open s
source
theorem is_open.subset_interior_iff {α : Type u} [topological_space α] {s t : set α} (h₁ : is_open s) :
s ⊆ interior t ↔ s ⊆ t
source
theorem subset_interior_iff {α : Type u} [topological_space α] {s t : set α} :
t ⊆ interior s ↔ ∃ (U : set α), is_open U ∧ t ⊆ U ∧ U ⊆ s
source
theorem interior_mono {α : Type u} [topological_space α] {s t : set α} (h : s ⊆ t) :
interior s ⊆ interior t
source
@[simp]
theorem interior_empty {α : Type u} [topological_space α] :
interior ∅ = ∅
source
@[simp]
theorem interior_univ {α : Type u} [topological_space α] :
interior set.univ = set.univ
source
@[simp]
theorem interior_eq_univ {α : Type u} [topological_space α] {s : set α} :
interior s = set.univ ↔ s = set.univ
source
@[simp]
theorem interior_interior {α : Type u} [topological_space α] {s : set α} :
interior (interior s) = interior s
source
@[simp]
theorem interior_inter {α : Type u} [topological_space α] {s t : set α} :
interior (s ∩ t) = interior s ∩ interior t
source
@[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)
source
@[simp]
theorem interior_Inter {α : Type u} [topological_space α] {ι : Type u_1} [finite ι] (f : ι → set α) :
interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
source
theorem interior_union_is_closed_of_interior_empty {α : Type u} [topological_space α] {s t : set α} (h₁ : is_closed s) (h₂ : interior t = ∅) :
interior (s ∪ t) = interior s
source
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)
source
theorem interior_Inter_subset {α : Type u} {ι : Sort w} [topological_space α] (s : ι → set α) :
interior (⋂ (i : ι), s i) ⊆ ⋂ (i : ι), interior (s i)
source
theorem interior_Inter₂_subset {α : Type u} {ι : Sort w} [topological_space α] (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)
source
theorem interior_sInter_subset {α : Type u} [topological_space α] (S : set (set α)) :
interior (⋂₀ S) ⊆ ⋂ (s : set α) (H : s ∈ S), interior s

Closure of a set #

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

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

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

Alias of the forward direction of closure_nonempty_iff.

source
theorem set.nonempty.closure {α : Type u} [topological_space α] {s : set α} :
s.nonempty → (closure s).nonempty

Alias of the reverse direction of closure_nonempty_iff.

source
@[simp]
theorem closure_univ {α : Type u} [topological_space α] :
closure set.univ = set.univ
source
@[simp]
theorem closure_closure {α : Type u} [topological_space α] {s : set α} :
closure (closure s) = closure s
source
@[simp]
theorem closure_union {α : Type u} [topological_space α] {s t : set α} :
closure (s ∪ t) = closure s ∪ closure t
source
@[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)
source
@[simp]
theorem closure_Union {α : Type u} [topological_space α] {ι : Type u_1} [finite ι] (f : ι → set α) :
closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
source
theorem interior_subset_closure {α : Type u} [topological_space α] {s : set α} :
interior s ⊆ closure s
source
theorem closure_eq_compl_interior_compl {α : Type u} [topological_space α] {s : set α} :
closure s = (interior sᶜ)ᶜ
source
@[simp]
theorem interior_compl {α : Type u} [topological_space α] {s : set α} :
interior sᶜ = (closure s)ᶜ
source
@[simp]
theorem closure_compl {α : Type u} [topological_space α] {s : set α} :
closure sᶜ = (interior s)ᶜ
source
theorem mem_closure_iff {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ closure s ↔ ∀ (o : set α), is_open o → a ∈ o → (o ∩ s).nonempty
source
theorem closure_inter_open_nonempty_iff {α : Type u} [topological_space α] {s t : set α} (h : is_open t) :
(closure s ∩ t).nonempty ↔ (s ∩ t).nonempty
source
theorem filter.le_lift'_closure {α : Type u} [topological_space α] (l : filter α) :
l ≤ l.lift' closure
source
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))
source
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 i → is_closed (s i)) :
l.lift' closure = l
source
@[simp]
theorem filter.lift'_closure_eq_bot {α : Type u} [topological_space α] {l : filter α} :
l.lift' closure = ⊥ ↔ l = ⊥
source
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
source
theorem dense_iff_closure_eq {α : Type u} [topological_space α] {s : set α} :
dense s ↔ closure s = set.univ
source
theorem dense.closure_eq {α : Type u} [topological_space α] {s : set α} (h : dense s) :
closure s = set.univ
source
theorem interior_eq_empty_iff_dense_compl {α : Type u} [topological_space α] {s : set α} :
interior s = ∅ ↔ dense sᶜ
source
theorem dense.interior_compl {α : Type u} [topological_space α] {s : set α} (h : dense s) :
interior sᶜ = ∅
source
@[simp]
theorem dense_closure {α : Type u} [topological_space α] {s : set α} :
dense (closure s) ↔ dense s

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

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

Alias of the forward direction of dense_closure.

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

Alias of the reverse direction of dense_closure.

source
@[simp]
theorem dense_univ {α : Type u} [topological_space α] :
dense set.univ
source
theorem dense_iff_inter_open {α : Type u} [topological_space α] {s : set α} :
dense s ↔ ∀ (U : set α), is_open U → U.nonempty → (U ∩ s).nonempty

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

source
theorem dense.inter_open_nonempty {α : Type u} [topological_space α] {s : set α} :
dense s → ∀ (U : set α), is_open U → U.nonempty → (U ∩ s).nonempty

Alias of the forward direction of dense_iff_inter_open.

source
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
source
theorem dense.nonempty_iff {α : Type u} [topological_space α] {s : set α} (hs : dense s) :
s.nonempty ↔ nonempty α
source
theorem dense.nonempty {α : Type u} [topological_space α] [h : nonempty α] {s : set α} (hs : dense s) :
s.nonempty
source
theorem dense.mono {α : Type u} [topological_space α] {s₁ s₂ : set α} (h : s₁ ⊆ s₂) (hd : dense s₁) :
dense s₂
source
theorem dense_compl_singleton_iff_not_open {α : Type u} [topological_space α] {x : α} :
dense {x}ᶜ ↔ ¬is_open {x}

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

Frontier of a set #

source
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
source
@[simp]
theorem closure_diff_interior {α : Type u} [topological_space α] (s : set α) :
closure s \ interior s = frontier s
source
@[simp]
theorem closure_diff_frontier {α : Type u} [topological_space α] (s : set α) :
closure s \ frontier s = interior s
source
@[simp]
theorem self_diff_frontier {α : Type u} [topological_space α] (s : set α) :
s \ frontier s = interior s
source
theorem frontier_eq_closure_inter_closure {α : Type u} [topological_space α] {s : set α} :
frontier s = closure s ∩ closure sᶜ
source
theorem frontier_subset_closure {α : Type u} [topological_space α] {s : set α} :
frontier s ⊆ closure s
source
theorem is_closed.frontier_subset {α : Type u} {s : set α} [topological_space α] (hs : is_closed s) :
frontier s ⊆ s
source
theorem frontier_closure_subset {α : Type u} [topological_space α] {s : set α} :
frontier (closure s) ⊆ frontier s
source
theorem frontier_interior_subset {α : Type u} [topological_space α] {s : set α} :
frontier (interior s) ⊆ frontier s
source
@[simp]
theorem frontier_compl {α : Type u} [topological_space α] (s : set α) :
frontier sᶜ = frontier s

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

source
@[simp]
theorem frontier_univ {α : Type u} [topological_space α] :
frontier set.univ = ∅
source
@[simp]
theorem frontier_empty {α : Type u} [topological_space α] :
frontier ∅ = ∅
source
theorem frontier_inter_subset {α : Type u} [topological_space α] (s t : set α) :
frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t
source
theorem frontier_union_subset {α : Type u} [topological_space α] (s t : set α) :
frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t
source
theorem is_closed.frontier_eq {α : Type u} [topological_space α] {s : set α} (hs : is_closed s) :
frontier s = s \ interior s
source
theorem is_open.frontier_eq {α : Type u} [topological_space α] {s : set α} (hs : is_open s) :
frontier s = closure s \ s
source
theorem is_open.inter_frontier_eq {α : Type u} [topological_space α] {s : set α} (hs : is_open s) :
s ∩ frontier s = ∅
source
theorem is_closed_frontier {α : Type u} [topological_space α] {s : set α} :
is_closed (frontier s)

The frontier of a set is closed.

source
theorem interior_frontier {α : Type u} [topological_space α] {s : set α} (h : is_closed s) :
interior (frontier s) = ∅

The frontier of a closed set has no interior point.

source
theorem closure_eq_interior_union_frontier {α : Type u} [topological_space α] (s : set α) :
closure s = interior s ∪ frontier s
source
theorem closure_eq_self_union_frontier {α : Type u} [topological_space α] (s : set α) :
closure s = s ∪ frontier s
source
theorem disjoint.frontier_left {α : Type u} {s t : set α} [topological_space α] (ht : is_open t) (hd : disjoint s t) :
disjoint (frontier s) t
source
theorem disjoint.frontier_right {α : Type u} {s t : set α} [topological_space α] (hs : is_open s) (hd : disjoint s t) :
disjoint s (frontier t)
source
theorem frontier_eq_inter_compl_interior {α : Type u} [topological_space α] {s : set α} :
frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ
source
theorem compl_frontier_eq_union_interior {α : Type u} [topological_space α] {s : set α} :
(frontier s)ᶜ = interior s ∪ interior sᶜ

Neighborhoods #

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

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

Equations
Instances for nhds
source
def nhds_within {α : Type u} [topological_space α] (a : α) (s : set α) :
filter α

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

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

source
theorem nhds_basis_closeds {α : Type u} [topological_space α] (a : α) :
(nhds a).has_basis (λ (s : set α), a ∉ s ∧ is_closed s) has_compl.compl
source
theorem le_nhds_iff {α : Type u} [topological_space α] {f : filter α} {a : α} :
f ≤ nhds a ↔ ∀ (s : set α), a ∈ s → is_open s → s ∈ f

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

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

source
theorem mem_nhds_iff {α : Type u} [topological_space α] {a : α} {s : set α} :
s ∈ nhds a ↔ ∃ (t : set α) (H : t ⊆ s), is_open t ∧ a ∈ t
source
theorem eventually_nhds_iff {α : Type u} [topological_space α] {a : α} {p : α → Prop} :
(∀ᶠ (x : α) in nhds a, p x) ↔ ∃ (t : set α), (∀ (x : α), x ∈ t → p 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.

source
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)
source
theorem mem_of_mem_nhds {α : Type u} [topological_space α] {a : α} {s : set α} :
s ∈ nhds a → a ∈ s
source
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.

source
theorem is_open.mem_nhds {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_open s) (ha : a ∈ s) :
s ∈ nhds a
source
theorem is_open.mem_nhds_iff {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_open s) :
s ∈ nhds a ↔ a ∈ s
source
theorem is_closed.compl_mem_nhds {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_closed s) (ha : a ∉ s) :
sᶜ ∈ nhds a
source
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
source
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.

source
theorem exists_open_set_nhds {α : Type u} [topological_space α] {s U : set α} (h : ∀ (x : α), x ∈ s → U ∈ 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.

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

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

source
@[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
source
@[simp]
theorem frequently_frequently_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} :
(∃ᶠ (y : α) in nhds a, ∃ᶠ (x : α) in nhds y, p x) ↔ ∃ᶠ (x : α) in nhds a, p x
source
@[simp]
theorem eventually_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
(∀ᶠ (x : α) in nhds a, s ∈ nhds x) ↔ s ∈ nhds a
source
@[simp]
theorem nhds_bind_nhds {α : Type u} {a : α} [topological_space α] :
(nhds a).bind nhds = nhds a
source
@[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
source
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
source
@[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
source
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.

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

source
theorem all_mem_nhds {α : Type u} [topological_space α] (x : α) (P : set α → Prop) (hP : ∀ (s t : set α), s ⊆ t → P s → P t) :
(∀ (s : set α), s ∈ nhds x → P s) ↔ ∀ (s : set α), is_open s → x ∈ s → P s
source
theorem all_mem_nhds_filter {α : Type u} {β : Type v} [topological_space α] (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 α), is_open s → x ∈ s → f s ∈ l
source
theorem tendsto_nhds {α : Type u} {β : Type v} [topological_space α] {f : β → α} {l : filter β} {a : α} :
filter.tendsto f l (nhds a) ↔ ∀ (s : set α), is_open s → a ∈ s → f ⁻¹' s ∈ l
source
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 ∈ U → is_open U → (∃ (N : β), ∀ (n : β), N ≤ n → f n ∈ U)
source
theorem tendsto_const_nhds {α : Type u} {β : Type v} [topological_space α] {a : α} {f : filter β} :
filter.tendsto (λ (b : β), a) f (nhds a)
source
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) :
filter.tendsto u filter.at_top (nhds x)
source
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) :
filter.tendsto u filter.at_bot (nhds x)
source
theorem pure_le_nhds {α : Type u} [topological_space α] :
has_pure.pure ≤ nhds
source
theorem tendsto_pure_nhds {β : Type v} {α : Type u_1} [topological_space β] (f : α → β) (a : α) :
filter.tendsto f (has_pure.pure a) (nhds (f a))
source
theorem order_top.tendsto_at_top_nhds {β : Type v} {α : Type u_1} [partial_order α] [order_top α] [topological_space β] (f : α → β) :
filter.tendsto f filter.at_top (nhds (f ⊤))
source
@[protected, simp, instance]
def nhds_ne_bot {α : Type u} [topological_space α] {a : α} :
(nhds a).ne_bot

Cluster points #

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

source
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, but beware that terminology varies. This is not the same as asking 𝓝[≠] x ⊓ F ≠ ⊥. See mem_closure_iff_cluster_pt in particular.

Equations
source
theorem cluster_pt.ne_bot {α : Type u} [topological_space α] {x : α} {F : filter α} (h : cluster_pt x F) :
(nhds x ⊓ F).ne_bot
source
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
source
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
source
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. See also mem_closure_iff_cluster_pt.

source
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
source
theorem cluster_pt.of_le_nhds {α : Type u} [topological_space α] {x : α} {f : filter α} (H : f ≤ nhds x) [f.ne_bot] :
cluster_pt x f
source
theorem cluster_pt.of_le_nhds' {α : Type u} [topological_space α] {x : α} {f : filter α} (H : f ≤ nhds x) (hf : f.ne_bot) :
cluster_pt x f
source
theorem cluster_pt.of_nhds_le {α : Type u} [topological_space α] {x : α} {f : filter α} (H : nhds x ≤ f) :
cluster_pt x f
source
theorem cluster_pt.mono {α : Type u} [topological_space α] {x : α} {f g : filter α} (H : cluster_pt x f) (h : f ≤ g) :
cluster_pt x g
source
theorem cluster_pt.of_inf_left {α : Type u} [topological_space α] {x : α} {f g : filter α} (H : cluster_pt x (f ⊓ g)) :
cluster_pt x f
source
theorem cluster_pt.of_inf_right {α : Type u} [topological_space α] {x : α} {f g : filter α} (H : cluster_pt x (f ⊓ g)) :
cluster_pt x g
source
theorem ultrafilter.cluster_pt_iff {α : Type u} [topological_space α] {x : α} {f : ultrafilter α} :
cluster_pt x ↑f ↔ ↑f ≤ nhds x
source
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
source
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)
source
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)) :
map_cluster_pt x F u
source
def acc_pt {α : Type u} [topological_space α] (x : α) (F : filter α) :
Prop

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

Equations
source
theorem acc_iff_cluster {α : Type u} [topological_space α] (x : α) (F : filter α) :
acc_pt x F ↔ cluster_pt x (filter.principal {x}ᶜ ⊓ F)
source
theorem acc_principal_iff_cluster {α : Type u} [topological_space α] (x : α) (C : set α) :
acc_pt x (filter.principal C) ↔ cluster_pt x (filter.principal (C \ {x}))

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

source
theorem acc_pt_iff_nhds {α : Type u} [topological_space α] (x : α) (C : set α) :
acc_pt x (filter.principal C) ↔ ∀ (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.

source
theorem acc_pt_iff_frequently {α : Type u} [topological_space α] (x : α) (C : set α) :
acc_pt x (filter.principal C) ↔ ∃ᶠ (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.

source
theorem acc_pt.mono {α : Type u} [topological_space α] {x : α} {F G : filter α} (h : acc_pt x F) (hFG : F ≤ G) :
acc_pt x 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 #

source
theorem interior_eq_nhds' {α : Type u} [topological_space α] {s : set α} :
interior s = {a : α | s ∈ nhds a}
source
theorem interior_eq_nhds {α : Type u} [topological_space α] {s : set α} :
interior s = {a : α | nhds a ≤ filter.principal s}
source
theorem mem_interior_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ interior s ↔ s ∈ nhds a
source
@[simp]
theorem interior_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
interior s ∈ nhds a ↔ s ∈ nhds a
source
theorem interior_set_of_eq {α : Type u} [topological_space α] {p : α → Prop} :
interior {x : α | p x} = {x : α | ∀ᶠ (y : α) in nhds x, p y}
source
theorem is_open_set_of_eventually_nhds {α : Type u} [topological_space α] {p : α → Prop} :
is_open {x : α | ∀ᶠ (y : α) in nhds x, p y}
source
theorem subset_interior_iff_nhds {α : Type u} [topological_space α] {s V : set α} :
s ⊆ interior V ↔ ∀ (x : α), x ∈ s → V ∈ nhds x
source
theorem is_open_iff_nhds {α : Type u} [topological_space α] {s : set α} :
is_open s ↔ ∀ (a : α), a ∈ s → nhds a ≤ filter.principal s
source
theorem is_open_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} :
is_open s ↔ ∀ (a : α), a ∈ s → s ∈ nhds a
source
theorem is_open_iff_eventually {α : Type u} [topological_space α] {s : set α} :
is_open s ↔ ∀ (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.

source
theorem is_open_iff_ultrafilter {α : Type u} [topological_space α] {s : set α} :
is_open s ↔ ∀ (x : α), x ∈ s → ∀ (l : ultrafilter α), ↑l ≤ nhds x → s ∈ l
source
theorem is_open_singleton_iff_nhds_eq_pure {α : Type u} [topological_space α] (a : α) :
is_open {a} ↔ nhds a = has_pure.pure a
source
theorem is_open_singleton_iff_punctured_nhds {α : Type u_1} [topological_space α] (a : α) :
is_open {a} ↔ nhds_within a {a}ᶜ = ⊥
source
theorem mem_closure_iff_frequently {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ closure s ↔ ∃ᶠ (x : α) in nhds a, x ∈ s
source
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.

source
theorem is_closed_iff_frequently {α : Type u} [topological_space α] {s : set α} :
is_closed s ↔ ∀ (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.

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

source
theorem mem_closure_iff_cluster_pt {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ closure s ↔ cluster_pt a (filter.principal s)
source
theorem mem_closure_iff_nhds_ne_bot {α : Type u} {a : α} [topological_space α] {s : set α} :
a ∈ closure s ↔ nhds a ⊓ filter.principal s ≠ ⊥
source
theorem mem_closure_iff_nhds_within_ne_bot {α : Type u} [topological_space α] {s : set α} {x : α} :
x ∈ closure s ↔ (nhds_within x s).ne_bot
source
theorem dense_compl_singleton {α : Type u} [topological_space α] (x : α) [(nhds_within x {x}ᶜ).ne_bot] :
dense {x}ᶜ

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

source
@[simp]
theorem closure_compl_singleton {α : Type u} [topological_space α] (x : α) [(nhds_within x {x}ᶜ).ne_bot] :
closure {x}ᶜ = set.univ

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

source
@[simp]
theorem interior_singleton {α : Type u} [topological_space α] (x : α) [(nhds_within x {x}ᶜ).ne_bot] :
interior {x} = ∅

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

source
theorem not_is_open_singleton {α : Type u} [topological_space α] (x : α) [(nhds_within x {x}ᶜ).ne_bot] :
¬is_open {x}
source
theorem closure_eq_cluster_pts {α : Type u} [topological_space α] {s : set α} :
closure s = {a : α | cluster_pt a (filter.principal s)}
source
theorem mem_closure_iff_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ closure s ↔ ∀ (t : set α), t ∈ nhds a → (t ∩ s).nonempty
source
theorem mem_closure_iff_nhds' {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ closure s ↔ ∀ (t : set α), t ∈ nhds a → (∃ (y : ↥s), ↑y ∈ t)
source
theorem mem_closure_iff_comap_ne_bot {α : Type u} [topological_space α] {A : set α} {x : α} :
x ∈ closure A ↔ (filter.comap coe (nhds x)).ne_bot
source
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
source
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)
source
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.

source
theorem is_closed_iff_cluster_pt {α : Type u} [topological_space α] {s : set α} :
is_closed s ↔ ∀ (a : α), cluster_pt a (filter.principal s) → a ∈ s
source
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
source
theorem is_closed.interior_union_left {α : Type u} [topological_space α] {s t : set α} (h : is_closed s) :
interior (s ∪ t) ⊆ s ∪ interior t
source
theorem is_closed.interior_union_right {α : Type u} [topological_space α] {s t : set α} (h : is_closed t) :
interior (s ∪ t) ⊆ interior s ∪ t
source
theorem is_open.inter_closure {α : Type u} [topological_space α] {s t : set α} (h : is_open s) :
s ∩ closure t ⊆ closure (s ∩ t)
source
theorem is_open.closure_inter {α : Type u} [topological_space α] {s t : set α} (h : is_open t) :
closure s ∩ t ⊆ closure (s ∩ t)
source
theorem dense.open_subset_closure_inter {α : Type u} [topological_space α] {s t : set α} (hs : dense s) (ht : is_open t) :
t ⊆ closure (t ∩ s)
source
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₂
source
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.

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

source
theorem dense.inter_nhds_nonempty {α : Type u} [topological_space α] {s t : set α} (hs : dense s) {x : α} (ht : t ∈ nhds x) :
(s ∩ t).nonempty
source
theorem closure_diff {α : Type u} [topological_space α] {s t : set α} :
closure s \ closure t ⊆ closure (s \ t)
source
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
source
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
source
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
source
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)) :
a ∈ closure s
source
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) :
a ∈ closure s
source
theorem tendsto_inf_principal_nhds_iff_of_forall_eq {α : Type u} {β : Type v} [topological_space α] {f : β → α} {l : filter β} {s : set β} {a : α} (h : ∀ (x : β), x ∉ s → f x = a) :
filter.tendsto f (l ⊓ filter.principal s) (nhds a) ↔ filter.tendsto f l (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 #

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

source
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 #

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

source
theorem continuous_def {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ↔ ∀ (s : set β), is_open s → is_open (f ⁻¹' s)
source
theorem is_open.preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set β} (h : is_open s) :
is_open (f ⁻¹' s)
source
theorem continuous.congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} (h : continuous f) (h' : ∀ (x : α), f x = g x) :
continuous g
source
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
source
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))
source
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
source
theorem continuous_at_congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {x : α} (h : f =ᶠ[nhds x] g) :
continuous_at f x ↔ continuous_at g x
source
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) :
continuous_at g x
source
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)) :
f ⁻¹' t ∈ nhds x
source
theorem eventually_eq_zero_nhds {α : Type u_1} [topological_space α] {M₀ : Type u_2} [has_zero M₀] {a : α} {f : α → M₀} :
f =ᶠ[nhds a] 0 ↔ a ∉ closure (function.support f)
source
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
source
theorem preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set β} (hf : continuous f) :
f ⁻¹' interior s ⊆ interior (f ⁻¹' s)

See also interior_preimage_subset_preimage_interior.

source
@[continuity]
theorem continuous_id {α : Type u_1} [topological_space α] :
continuous id
source
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) :
continuous (g ∘ f)
source
theorem continuous.iterate {α : Type u_1} [topological_space α] {f : α → α} (h : continuous f) (n : ℕ) :
continuous f^[n]
source
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) :
continuous_at (g ∘ f) x
source
theorem continuous_at.comp_of_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {x : α} {y : β} (hg : continuous_at g y) (hf : continuous_at f x) (hy : f x = y) :
continuous_at (g ∘ f) x

See note [comp_of_eq lemmas]

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

source
theorem continuous.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} (h : continuous f) :
continuous_at f x
source
theorem continuous_iff_continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ↔ ∀ (x : α), continuous_at f x
source
theorem continuous_at_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {b : β} :
continuous_at (λ (a : α), b) x
source
@[continuity]
theorem continuous_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {b : β} :
continuous (λ (a : α), b)
source
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) :
continuous_at f x
source
theorem continuous_of_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (h : ∀ (x y : α), f x = f y) :
continuous f
source
theorem continuous_at_id {α : Type u_1} [topological_space α] {x : α} :
continuous_at id x
source
theorem continuous_at.iterate {α : Type u_1} [topological_space α] {f : α → α} {x : α} (hf : continuous_at f x) (hx : f x = x) (n : ℕ) :
continuous_at f^[n] x
source
theorem continuous_iff_is_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ↔ ∀ (s : set β), is_closed s → is_closed (f ⁻¹' s)
source
theorem is_closed.preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set β} (h : is_closed s) :
is_closed (f ⁻¹' s)
source
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)
source
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 x → filter.tendsto f ↑g (nhds (f x))
source
theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ↔ ∀ (x : α) (g : ultrafilter α), ↑g ≤ nhds x → filter.tendsto f ↑g (nhds (f x))
source
theorem continuous.closure_preimage_subset {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (t : set β) :
closure (f ⁻¹' t) ⊆ f ⁻¹' closure t
source
theorem continuous.frontier_preimage_subset {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (t : set β) :
frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t
source
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) :
set.maps_to f (closure s) (closure t)

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

source
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)
source
theorem closure_subset_preimage_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} (h : continuous f) :
closure s ⊆ f ⁻¹' closure (f '' s)
source
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 : set.maps_to f s t) :
f a ∈ closure t
source
theorem set.maps_to.closure_left {α : 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) (ht : is_closed t) :
set.maps_to f (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 #

source
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
source
theorem function.surjective.dense_range {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} (hf : function.surjective f) :
dense_range f

A surjective map has dense range.

source
theorem dense_range_id {α : Type u_1} [topological_space α] :
dense_range id
source
theorem dense_range_iff_closure_range {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} :
dense_range f ↔ closure (set.range f) = set.univ
source
theorem dense_range.closure_range {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} (h : dense_range f) :
closure (set.range f) = set.univ
source
theorem dense.dense_range_coe {α : Type u_1} [topological_space α] {s : set α} (h : dense s) :
dense_range coe
source
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) :
set.range f ⊆ closure (f '' s)
source
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.

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

source
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) :
dense t

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

source
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) :
dense_range (g ∘ f)

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

source
theorem dense_range.nonempty_iff {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} (hf : dense_range f) :
nonempty κ ↔ nonempty β
source
theorem dense_range.nonempty {β : Type u_2} [topological_space β] {κ : Type u_5} {f : κ → β} [h : nonempty β] (hf : dense_range f) :
nonempty κ
source
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
source
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
source
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
source
def library_note.continuity lemma statement  :
unit

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

source
def library_note.comp_of_eq lemmas  :
unit

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