mathlib documentation

topology.basic

Basic theory of topological spaces. #

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

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

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

Notation #

Implementation notes #

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

References #

Tags #

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

Topological spaces #

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

A topology on α.

Instances
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
@[ext]
theorem topological_space_eq {α : Type u} {f g : topological_space α} :
f.is_open = g.is_open → f = g
source
def is_open {α : Type u} [t : topological_space α] (s : set α) :
Prop

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

Equations
source
@[simp]
theorem is_open_univ {α : Type u} [t : topological_space α] :
is_open set.univ
source
theorem is_open.inter {α : Type u} {s₁ s₂ : set α} [t : topological_space α] (h₁ : is_open s₁) (h₂ : is_open s₂) :
is_open (s₁ ∩ s₂)
source
theorem is_open_sUnion {α : Type u} [t : topological_space α] {s : set (set α)} (h : ∀ (t_1 : set α), t_1 ∈ s → is_open t_1) :
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 α} :
t.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} {β : Type v} [topological_space α] [fintype β] {s : β → set α} (h : ∀ (i : β), is_open (s i)) :
is_open (⋂ (i : β), s i)
source
theorem is_open_Inter_prop {α : Type u} [topological_space α] {p : Prop} {s : p → set α} (h : ∀ (h : p), is_open (s h)) :
is_open (set.Inter s)
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

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} {β : Type v} [topological_space α] [fintype β] {s : β → set α} (h : ∀ (i : β), is_closed (s i)) :
is_closed (set.Union s)
source
theorem is_closed_Union_prop {α : Type u} [topological_space α] {p : Prop} {s : p → set α} (h : ∀ (h : p), is_closed (s h)) :
is_closed (set.Union s)
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_open {α : Type u} [topological_space α] {s : set α} :
interior s = s ↔ is_open s
source
theorem subset_interior_iff_open {α : Type u} [topological_space α] {s : set α} :
s ⊆ interior s ↔ is_open s
source
theorem subset_interior_iff_subset_of_open {α : 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_of_fintype {α : Type u} [topological_space α] {ι : Type u_1} [fintype ι] (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_1} [topological_space α] {U : set α} (hU : is_closed U) {x : α} :
x ∈ U ↔ closure {x} ⊆ U
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 closure_nonempty_iff.

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

Alias 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_of_fintype {α : Type u} [topological_space α] {ι : Type u_1} [fintype ι] (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
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 dense_closure.

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

Alias 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 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
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 is_open.inter_frontier_eq_empty_of_disjoint {α : Type u} [topological_space α] {s t : set α} (ht : is_open t) (hd : disjoint s t) :
t ∩ frontier s = ∅
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
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
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
source
theorem nhds_def {α : Type u} [topological_space α] (a : α) :
𝓝 a = ⨅ (s : set α) (H : s ∈ {s : set α | a ∈ s ∧ is_open s}), 𝓟 s
source
theorem nhds_basis_opens {α : Type u} [topological_space α] (a : α) :
(𝓝 a).has_basis (λ (s : set α), a ∈ s ∧ is_open s) (λ (x : set α), x)

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

source
theorem le_nhds_iff {α : Type u} [topological_space α] {f : filter α} {a : α} :
f ≤ 𝓝 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 : 𝓟 s ≤ f) :
𝓝 a ≤ f

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

source
theorem mem_nhds_iff {α : Type u} [topological_space α] {a : α} {s : set α} :
s ∈ 𝓝 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 𝓝 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 (𝓝 a) = ⨅ (s : set α) (H : s ∈ {s : set α | a ∈ s ∧ is_open s}), 𝓟 (f '' s)
source
theorem mem_of_mem_nhds {α : Type u} [topological_space α] {a : α} {s : set α} :
s ∈ 𝓝 a → a ∈ s
source
theorem filter.eventually.self_of_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} (h : ∀ᶠ (y : α) in 𝓝 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 ∈ 𝓝 a
source
theorem is_open.mem_nhds_iff {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_open s) :
s ∈ 𝓝 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ᶜ ∈ 𝓝 a
source
theorem is_open.eventually_mem {α : Type u} [topological_space α] {a : α} {s : set α} (hs : is_open s) (ha : a ∈ s) :
∀ᶠ (x : α) in 𝓝 a, x ∈ s
source
theorem nhds_basis_opens' {α : Type u} [topological_space α] (a : α) :
(𝓝 a).has_basis (λ (s : set α), s ∈ 𝓝 a ∧ is_open s) (λ (x : set α), x)

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

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

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

source
@[simp]
theorem eventually_eventually_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} :
(∀ᶠ (y : α) in 𝓝 a, ∀ᶠ (x : α) in 𝓝 y, p x) ↔ ∀ᶠ (x : α) in 𝓝 a, p x
source
@[simp]
theorem eventually_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
(∀ᶠ (x : α) in 𝓝 a, s ∈ 𝓝 x) ↔ s ∈ 𝓝 a
source
@[simp]
theorem nhds_bind_nhds {α : Type u} {a : α} [topological_space α] :
(𝓝 a).bind 𝓝 = 𝓝 a
source
@[simp]
theorem eventually_eventually_eq_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} :
(∀ᶠ (y : α) in 𝓝 a, f =ᶠ[𝓝 y] g) ↔ f =ᶠ[𝓝 a] g
source
theorem filter.eventually_eq.eq_of_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} (h : f =ᶠ[𝓝 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 𝓝 a, f ≤ᶠ[𝓝 y] g) ↔ f ≤ᶠ[𝓝 a] g
source
theorem filter.eventually_eq.eventually_eq_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} (h : f =ᶠ[𝓝 a] g) :
∀ᶠ (y : α) in 𝓝 a, f =ᶠ[𝓝 y] g

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

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

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

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 ∈ 𝓝 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 ∈ 𝓝 x → f s ∈ l) ↔ ∀ (s : set α), is_open s → x ∈ s → f s ∈ l
source
theorem rtendsto_nhds {α : Type u} {β : Type v} [topological_space α] {r : rel β α} {l : filter β} {a : α} :
filter.rtendsto r l (𝓝 a) ↔ ∀ (s : set α), is_open s → a ∈ s → r.core s ∈ l
source
theorem rtendsto'_nhds {α : Type u} {β : Type v} [topological_space α] {r : rel β α} {l : filter β} {a : α} :
filter.rtendsto' r l (𝓝 a) ↔ ∀ (s : set α), is_open s → a ∈ s → r.preimage s ∈ l
source
theorem ptendsto_nhds {α : Type u} {β : Type v} [topological_space α] {f : β →. α} {l : filter β} {a : α} :
filter.ptendsto f l (𝓝 a) ↔ ∀ (s : set α), is_open s → a ∈ s → f.core s ∈ l
source
theorem ptendsto'_nhds {α : Type u} {β : Type v} [topological_space α] {f : β →. α} {l : filter β} {a : α} :
filter.ptendsto' f l (𝓝 a) ↔ ∀ (s : set α), is_open s → a ∈ s → f.preimage s ∈ l
source
theorem tendsto_nhds {α : Type u} {β : Type v} [topological_space α] {f : β → α} {l : filter β} {a : α} :
filter.tendsto f l (𝓝 a) ↔ ∀ (s : set α), is_open s → a ∈ s → f ⁻¹' s ∈ l
source
theorem tendsto_const_nhds {α : Type u} {β : Type v} [topological_space α] {a : α} {f : filter β} :
filter.tendsto (λ (b : β), a) f (𝓝 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 (𝓝 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 (𝓝 x)
source
theorem pure_le_nhds {α : Type u} [topological_space α] :
pure ≤ 𝓝
source
theorem tendsto_pure_nhds {β : Type v} {α : Type u_1} [topological_space β] (f : α → β) (a : α) :
filter.tendsto f (pure a) (𝓝 (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 (𝓝 (f ⊤))
source
@[protected, simp, instance]
def nhds_ne_bot {α : Type u} [topological_space α] {a : α} :
(𝓝 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.

Equations
source
theorem cluster_pt.ne_bot {α : Type u} [topological_space α] {x : α} {F : filter α} (h : cluster_pt x F) :
(𝓝 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 : (𝓝 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 ∈ 𝓝 x → ∀ ⦃V : set α⦄, V ∈ F → (U ∩ V).nonempty
source
theorem cluster_pt_principal_iff {α : Type u} [topological_space α] {x : α} {s : set α} :
cluster_pt x (𝓟 s) ↔ ∀ (U : set α), U ∈ 𝓝 x → (U ∩ s).nonempty

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

source
theorem cluster_pt_principal_iff_frequently {α : Type u} [topological_space α] {x : α} {s : set α} :
cluster_pt x (𝓟 s) ↔ ∃ᶠ (y : α) in 𝓝 x, y ∈ s
source
theorem cluster_pt.of_le_nhds {α : Type u} [topological_space α] {x : α} {f : filter α} (H : f ≤ 𝓝 x) [f.ne_bot] :
cluster_pt x f
source
theorem cluster_pt.of_le_nhds' {α : Type u} [topological_space α] {x : α} {f : filter α} (H : f ≤ 𝓝 x) (hf : f.ne_bot) :
cluster_pt x f
source
theorem cluster_pt.of_nhds_le {α : Type u} [topological_space α] {x : α} {f : filter α} (H : 𝓝 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 ≤ 𝓝 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 ∈ 𝓝 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 (𝓝 x)) :
map_cluster_pt x F u

Interior, closure and frontier in terms of neighborhoods #

source
theorem interior_eq_nhds' {α : Type u} [topological_space α] {s : set α} :
interior s = {a : α | s ∈ 𝓝 a}
source
theorem interior_eq_nhds {α : Type u} [topological_space α] {s : set α} :
interior s = {a : α | 𝓝 a ≤ 𝓟 s}
source
theorem mem_interior_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ interior s ↔ s ∈ 𝓝 a
source
@[simp]
theorem interior_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
interior s ∈ 𝓝 a ↔ s ∈ 𝓝 a
source
theorem interior_set_of_eq {α : Type u} [topological_space α] {p : α → Prop} :
interior {x : α | p x} = {x : α | ∀ᶠ (y : α) in 𝓝 x, p y}
source
theorem is_open_set_of_eventually_nhds {α : Type u} [topological_space α] {p : α → Prop} :
is_open {x : α | ∀ᶠ (y : α) in 𝓝 x, p y}
source
theorem subset_interior_iff_nhds {α : Type u} [topological_space α] {s V : set α} :
s ⊆ interior V ↔ ∀ (x : α), x ∈ s → V ∈ 𝓝 x
source
theorem is_open_iff_nhds {α : Type u} [topological_space α] {s : set α} :
is_open s ↔ ∀ (a : α), a ∈ s → 𝓝 a ≤ 𝓟 s
source
theorem is_open_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} :
is_open s ↔ ∀ (a : α), a ∈ s → s ∈ 𝓝 a
source
theorem is_open_iff_ultrafilter {α : Type u} [topological_space α] {s : set α} :
is_open s ↔ ∀ (x : α), x ∈ s → ∀ (l : ultrafilter α), ↑l ≤ 𝓝 x → s ∈ l
source
theorem is_open_singleton_iff_nhds_eq_pure {α : Type u_1} [topological_space α] (a : α) :
is_open {a} ↔ 𝓝 a = pure a
source
theorem mem_closure_iff_frequently {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ closure s ↔ ∃ᶠ (x : α) in 𝓝 a, x ∈ s
source
theorem filter.frequently.mem_closure {α : Type u} [topological_space α] {s : set α} {a : α} :
(∃ᶠ (x : α) in 𝓝 a, x ∈ s) → a ∈ closure s

Alias of mem_closure_iff_frequently.

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 (𝓟 s)
source
theorem mem_closure_iff_nhds_ne_bot {α : Type u} {a : α} [topological_space α] {s : set α} :
a ∈ closure s ↔ 𝓝 a ⊓ 𝓟 s ≠ ⊥
source
theorem mem_closure_iff_nhds_within_ne_bot {α : Type u} [topological_space α] {s : set α} {x : α} :
x ∈ closure s ↔ (𝓝[s] x).ne_bot
source
theorem dense_compl_singleton {α : Type u} [topological_space α] (x : α) [(𝓝[{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 : α) [(𝓝[{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 : α) [(𝓝[{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 closure_eq_cluster_pts {α : Type u} [topological_space α] {s : set α} :
closure s = {a : α | cluster_pt a (𝓟 s)}
source
theorem mem_closure_iff_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ closure s ↔ ∀ (t : set α), t ∈ 𝓝 a → (t ∩ s).nonempty
source
theorem mem_closure_iff_nhds' {α : Type u} [topological_space α] {s : set α} {a : α} :
a ∈ closure s ↔ ∀ (t : set α), t ∈ 𝓝 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 (𝓝 x)).ne_bot
source
theorem mem_closure_iff_nhds_basis' {α : Type u} {ι : Sort w} [topological_space α] {a : α} {p : ι → Prop} {s : ι → set α} (h : (𝓝 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 : (𝓝 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 ≤ 𝓝 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 (𝓟 s) → a ∈ s
source
theorem is_closed_iff_nhds {α : Type u} [topological_space α] {s : set α} :
is_closed s ↔ ∀ (x : α), (∀ (U : set α), U ∈ 𝓝 x → (U ∩ s).nonempty) → x ∈ s
source
theorem closure_inter_open {α : Type u} [topological_space α] {s t : set α} (h : is_open s) :
s ∩ closure t ⊆ closure (s ∩ t)
source
theorem closure_inter_open' {α : 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₁ᶜ ∈ 𝓝 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 ∈ 𝓝 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 𝓝 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 (𝓝 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 (𝓝 a)) (h : ∀ᶠ (x : β) in b, f x ∈ s) :
a ∈ 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 (𝓝 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 ⊓ 𝓟 s) (𝓝 a) ↔ filter.tendsto f l (𝓝 a)

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

Limits of filters in topological spaces #

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 ≤ 𝓝 a) :
f ≤ 𝓝 (Lim f)

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

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

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

Locally finite families #

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

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

Equations
source
theorem locally_finite.point_finite {α : Type u} {β : Type v} [topological_space α] {f : β → set α} (hf : locally_finite f) (x : α) :
{b : β | x ∈ f b}.finite
source
theorem locally_finite_of_fintype {α : Type u} {β : Type v} [topological_space α] [fintype β] (f : β → set α) :
locally_finite f
source
theorem locally_finite.subset {α : Type u} {β : Type v} [topological_space α] {f₁ f₂ : β → set α} (hf₂ : locally_finite f₂) (hf : ∀ (b : β), f₁ b ⊆ f₂ b) :
locally_finite f₁
source
theorem locally_finite.comp_injective {α : Type u} {β : Type v} [topological_space α] {ι : Type u_1} {f : β → set α} {g : ι → β} (hf : locally_finite f) (hg : function.injective g) :
locally_finite (f ∘ g)
source
theorem locally_finite.closure {α : Type u} {β : Type v} [topological_space α] {f : β → set α} (hf : locally_finite f) :
locally_finite (λ (i : β), closure (f i))
source
theorem locally_finite.is_closed_Union {α : Type u} {β : Type v} [topological_space α] {f : β → set α} (h₁ : locally_finite f) (h₂ : ∀ (i : β), is_closed (f i)) :
is_closed (⋃ (i : β), f i)
source
theorem locally_finite.closure_Union {α : Type u} {β : Type v} [topological_space α] {f : β → set α} (h : locally_finite f) :
closure (⋃ (i : β), f i) = ⋃ (i : β), closure (f i)

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 (𝓝 x) (𝓝 (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 ∈ 𝓝 (f x) → f ⁻¹' A ∈ 𝓝 x
source
theorem continuous_at_congr {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f g : α → β} {x : α} (h : f =ᶠ[𝓝 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 =ᶠ[𝓝 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 ∈ 𝓝 (f x)) :
f ⁻¹' t ∈ 𝓝 x
source
theorem eventually_eq_zero_nhds {α : Type u_1} [topological_space α] {M₀ : Type u_2} [has_zero M₀] {a : α} {f : α → M₀} :
f =ᶠ[𝓝 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.tendsto {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (x : α) :
filter.tendsto f (𝓝 x) (𝓝 (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 (𝓝 x) (𝓝 y)

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

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 =ᶠ[𝓝 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 ≤ 𝓝 x → filter.tendsto f ↑g (𝓝 (f x))
source
theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :
continuous f ↔ ∀ (x : α) (g : ultrafilter α), ↑g ≤ 𝓝 x → filter.tendsto f ↑g (𝓝 (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

Continuity and partial functions #

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

Continuity of a partial function

Equations
source
theorem open_dom_of_pcontinuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} (h : pcontinuous f) :
is_open f.dom
source
theorem pcontinuous_iff' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} :
pcontinuous f ↔ ∀ {x : α} {y : β}, y ∈ f x → filter.ptendsto' f (𝓝 x) (𝓝 y)
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 : ∀ (a : α), a ∈ s → f a ∈ t) :
f a ∈ closure 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_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 ∈ 𝓝 b) :
∃ (a : κ), f a ∈ U