# Documentation

Mathlib.Topology.Basic

# Basic theory of topological spaces. #

The main definition is the type class TopologicalSpace α which endows a type α with a topology. Then Set α gets predicates IsOpen, IsClosed 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 ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥⊓ F ≠ ⊥≠ ⊥⊥. A map f : ι → α→ α clusters at x along F : Filter ι if MapClusterPt x F f : ClusterPt x (map f F). In particular the notion of cluster point of a sequence u is MapClusterPt x atTop u.

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

## Notation #

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

## Implementation notes #

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

## References #

• [N. Bourbaki, General Topology][bourbaki1966]
• [I. M. James, Topologies and Uniformities][james1999]

## Tags #

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

### Topological spaces #

class TopologicalSpace (α : Type u) :
• A predicate saying that a set is an open set. Use IsOpen in the root namespace instead.

IsOpen : Set αProp
• The set representing the whole space is an open set. Use isOpen_univ in the root namespace instead.

isOpen_univ : IsOpen Set.univ
• The intersection of two open sets is an open set. Use IsOpen.inter instead.

isOpen_inter : (s t : Set α) → IsOpen sIsOpen tIsOpen (s t)
• The union of a family of open sets is an open set. Use isOpen_unionₛ in the root namespace instead.

isOpen_unionₛ : (s : Set (Set α)) → ((t : Set α) → t sIsOpen t) → IsOpen (⋃₀ s)

A topology on α.

Instances
def TopologicalSpace.ofClosed {α : Type u} (T : Set (Set α)) (empty_mem : T) (sInter_mem : ∀ (A : Set (Set α)), A T⋂₀ A T) (union_mem : ∀ (A : Set α), A T∀ (B : Set α), B TA B T) :

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

Equations
• One or more equations did not get rendered due to their size.
def IsOpen {α : Type u} [inst : ] :
Set αProp

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

Equations
• IsOpen = TopologicalSpace.IsOpen

Notation for IsOpen with respect to a non-standard topology.

Equations
• One or more equations did not get rendered due to their size.
theorem isOpen_mk {α : Type u} {p : Set αProp} {h₁ : p Set.univ} {h₂ : (s t : Set α) → p sp tp (s t)} {h₃ : (s : Set (Set α)) → ((t : Set α) → t sp t) → p (⋃₀ s)} {s : Set α} :
p s
theorem topologicalSpace_eq {α : Type u} {f : } {g : } :
IsOpen = IsOpenf = g
@[simp]
theorem isOpen_univ {α : Type u} [inst : ] :
IsOpen Set.univ
theorem IsOpen.inter {α : Type u} {s₁ : Set α} {s₂ : Set α} [inst : ] (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) :
IsOpen (s₁ s₂)
theorem isOpen_unionₛ {α : Type u} [inst : ] {s : Set (Set α)} (h : ∀ (t : Set α), t s) :
theorem topologicalSpace_eq_iff {α : Type u} {t : } {t' : } :
t = t' ∀ (s : Set α),
theorem isOpen_fold {α : Type u} {s : Set α} {t : } :
theorem isOpen_unionᵢ {α : Type u} {ι : Sort w} [inst : ] {f : ιSet α} (h : ∀ (i : ι), IsOpen (f i)) :
IsOpen (Set.unionᵢ fun i => f i)
theorem isOpen_bunionᵢ {α : Type u} {β : Type v} [inst : ] {s : Set β} {f : βSet α} (h : ∀ (i : β), i sIsOpen (f i)) :
IsOpen (Set.unionᵢ fun i => Set.unionᵢ fun h => f i)
theorem IsOpen.union {α : Type u} {s₁ : Set α} {s₂ : Set α} [inst : ] (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) :
IsOpen (s₁ s₂)
@[simp]
theorem isOpen_empty {α : Type u} [inst : ] :
theorem isOpen_interₛ {α : Type u} [inst : ] {s : Set (Set α)} (hs : ) :
(∀ (t : Set α), t s) → IsOpen (⋂₀ s)
theorem isOpen_binterᵢ {α : Type u} {β : Type v} [inst : ] {s : Set β} {f : βSet α} (hs : ) (h : ∀ (i : β), i sIsOpen (f i)) :
IsOpen (Set.interᵢ fun i => Set.interᵢ fun h => f i)
theorem isOpen_interᵢ {α : Type u} {ι : Sort w} [inst : ] [inst : ] {s : ιSet α} (h : ∀ (i : ι), IsOpen (s i)) :
IsOpen (Set.interᵢ fun i => s i)
theorem isOpen_interᵢ_prop {α : Type u} [inst : ] {p : Prop} {s : pSet α} (h : ∀ (h : p), IsOpen (s h)) :
theorem isOpen_binterᵢ_finset {α : Type u} {β : Type v} [inst : ] {s : } {f : βSet α} (h : ∀ (i : β), i sIsOpen (f i)) :
IsOpen (Set.interᵢ fun i => Set.interᵢ fun h => f i)
@[simp]
theorem isOpen_const {α : Type u} [inst : ] {p : Prop} :
IsOpen { _a | p }
theorem IsOpen.and {α : Type u} {p₁ : αProp} {p₂ : αProp} [inst : ] :
IsOpen { a | p₁ a }IsOpen { a | p₂ a }IsOpen { a | p₁ a p₂ a }
class IsClosed {α : Type u} [inst : ] (s : Set α) :
• The complement of a closed set is an open set.

isOpen_compl : IsOpen (s)

A set is closed if its complement is open

Instances

Notation for IsClosed with respect to a non-standard topology.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem isOpen_compl_iff {α : Type u} [inst : ] {s : Set α} :
theorem isClosed_const {α : Type u} [inst : ] {p : Prop} :
IsClosed { _a | p }
@[simp]
theorem isClosed_empty {α : Type u} [inst : ] :
@[simp]
theorem isClosed_univ {α : Type u} [inst : ] :
IsClosed Set.univ
theorem IsClosed.union {α : Type u} {s₁ : Set α} {s₂ : Set α} [inst : ] :
IsClosed s₁IsClosed s₂IsClosed (s₁ s₂)
theorem isClosed_interₛ {α : Type u} [inst : ] {s : Set (Set α)} :
(∀ (t : Set α), t s) → IsClosed (⋂₀ s)
theorem isClosed_interᵢ {α : Type u} {ι : Sort w} [inst : ] {f : ιSet α} (h : ∀ (i : ι), IsClosed (f i)) :
IsClosed (Set.interᵢ fun i => f i)
theorem isClosed_binterᵢ {α : Type u} {β : Type v} [inst : ] {s : Set β} {f : βSet α} (h : ∀ (i : β), i sIsClosed (f i)) :
IsClosed (Set.interᵢ fun i => Set.interᵢ fun h => f i)
@[simp]
theorem isClosed_compl_iff {α : Type u} [inst : ] {s : Set α} :
theorem IsOpen.isClosed_compl {α : Type u} [inst : ] {s : Set α} :
IsClosed (s)

Alias of the reverse direction of isClosed_compl_iff.

theorem IsOpen.sdiff {α : Type u} [inst : ] {s : Set α} {t : Set α} (h₁ : ) (h₂ : ) :
IsOpen (s \ t)
theorem IsClosed.inter {α : Type u} {s₁ : Set α} {s₂ : Set α} [inst : ] (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) :
IsClosed (s₁ s₂)
theorem IsClosed.sdiff {α : Type u} [inst : ] {s : Set α} {t : Set α} (h₁ : ) (h₂ : ) :
IsClosed (s \ t)
theorem isClosed_bunionᵢ {α : Type u} {β : Type v} [inst : ] {s : Set β} {f : βSet α} (hs : ) (h : ∀ (i : β), i sIsClosed (f i)) :
IsClosed (Set.unionᵢ fun i => Set.unionᵢ fun h => f i)
theorem isClosed_unionᵢ {α : Type u} {ι : Sort w} [inst : ] [inst : ] {s : ιSet α} (h : ∀ (i : ι), IsClosed (s i)) :
IsClosed (Set.unionᵢ fun i => s i)
theorem isClosed_unionᵢ_prop {α : Type u} [inst : ] {p : Prop} {s : pSet α} (h : ∀ (h : p), IsClosed (s h)) :
theorem isClosed_imp {α : Type u} [inst : ] {p : αProp} {q : αProp} (hp : IsOpen { x | p x }) (hq : IsClosed { x | q x }) :
IsClosed { x | p xq x }
theorem IsClosed.not {α : Type u} {p : αProp} [inst : ] :
IsClosed { a | p a }IsOpen { a | ¬p a }

### Interior of a set #

def interior {α : Type u} [inst : ] (s : Set α) :
Set α

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

Equations
theorem mem_interior {α : Type u} [inst : ] {s : Set α} {x : α} :
x t, t s x t
@[simp]
theorem isOpen_interior {α : Type u} [inst : ] {s : Set α} :
theorem interior_subset {α : Type u} [inst : ] {s : Set α} :
s
theorem interior_maximal {α : Type u} [inst : ] {s : Set α} {t : Set α} (h₁ : t s) (h₂ : ) :
t
theorem IsOpen.interior_eq {α : Type u} [inst : ] {s : Set α} (h : ) :
= s
theorem interior_eq_iff_isOpen {α : Type u} [inst : ] {s : Set α} :
= s
theorem subset_interior_iff_isOpen {α : Type u} [inst : ] {s : Set α} :
s
theorem IsOpen.subset_interior_iff {α : Type u} [inst : ] {s : Set α} {t : Set α} (h₁ : ) :
s s t
theorem subset_interior_iff {α : Type u} [inst : ] {s : Set α} {t : Set α} :
t U, t U U s
theorem interior_mono {α : Type u} [inst : ] {s : Set α} {t : Set α} (h : s t) :
@[simp]
theorem interior_empty {α : Type u} [inst : ] :
@[simp]
theorem interior_univ {α : Type u} [inst : ] :
interior Set.univ = Set.univ
@[simp]
theorem interior_eq_univ {α : Type u} [inst : ] {s : Set α} :
= Set.univ s = Set.univ
@[simp]
theorem interior_interior {α : Type u} [inst : ] {s : Set α} :
@[simp]
theorem interior_inter {α : Type u} [inst : ] {s : Set α} {t : Set α} :
interior (s t) =
@[simp]
theorem Finset.interior_interᵢ {α : Type u} [inst : ] {ι : Type u_1} (s : ) (f : ιSet α) :
interior (Set.interᵢ fun i => Set.interᵢ fun h => f i) = Set.interᵢ fun i => Set.interᵢ fun h => interior (f i)
@[simp]
theorem interior_interᵢ {α : Type u} [inst : ] {ι : Type u_1} [inst : ] (f : ιSet α) :
interior (Set.interᵢ fun i => f i) = Set.interᵢ fun i => interior (f i)
theorem interior_union_isClosed_of_interior_empty {α : Type u} [inst : ] {s : Set α} {t : Set α} (h₁ : ) (h₂ : ) :
interior (s t) =
theorem isOpen_iff_forall_mem_open {α : Type u} {s : Set α} [inst : ] :
∀ (x : α), x st, t s x t
theorem interior_interᵢ_subset {α : Type u} {ι : Sort w} [inst : ] (s : ιSet α) :
interior (Set.interᵢ fun i => s i) Set.interᵢ fun i => interior (s i)
theorem interior_Inter₂_subset {α : Type u} {ι : Sort w} [inst : ] (p : ιSort u_1) (s : (i : ι) → p iSet α) :
interior (Set.interᵢ fun i => Set.interᵢ fun j => s i j) Set.interᵢ fun i => Set.interᵢ fun j => interior (s i j)
theorem interior_interₛ_subset {α : Type u} [inst : ] (S : Set (Set α)) :

### Closure of a set #

def closure {α : Type u} [inst : ] (s : Set α) :
Set α

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

Equations
@[simp]
theorem isClosed_closure {α : Type u} [inst : ] {s : Set α} :
theorem subset_closure {α : Type u} [inst : ] {s : Set α} :
s
theorem not_mem_of_not_mem_closure {α : Type u} [inst : ] {s : Set α} {P : α} (hP : ¬P ) :
¬P s
theorem closure_minimal {α : Type u} [inst : ] {s : Set α} {t : Set α} (h₁ : s t) (h₂ : ) :
t
theorem Disjoint.closure_left {α : Type u} [inst : ] {s : Set α} {t : Set α} (hd : Disjoint s t) (ht : ) :
theorem Disjoint.closure_right {α : Type u} [inst : ] {s : Set α} {t : Set α} (hd : Disjoint s t) (hs : ) :
theorem IsClosed.closure_eq {α : Type u} [inst : ] {s : Set α} (h : ) :
= s
theorem IsClosed.closure_subset {α : Type u} [inst : ] {s : Set α} (hs : ) :
s
theorem IsClosed.closure_subset_iff {α : Type u} [inst : ] {s : Set α} {t : Set α} (h₁ : ) :
t s t
theorem IsClosed.mem_iff_closure_subset {α : Type u} [inst : ] {s : Set α} (hs : ) {x : α} :
x s closure {x} s
theorem closure_mono {α : Type u} [inst : ] {s : Set α} {t : Set α} (h : s t) :
theorem monotone_closure (α : Type u_1) [inst : ] :
Monotone closure
theorem diff_subset_closure_iff {α : Type u} [inst : ] {s : Set α} {t : Set α} :
s \ t s
theorem closure_inter_subset_inter_closure {α : Type u} [inst : ] (s : Set α) (t : Set α) :
theorem isClosed_of_closure_subset {α : Type u} [inst : ] {s : Set α} (h : s) :
theorem closure_eq_iff_isClosed {α : Type u} [inst : ] {s : Set α} :
= s
theorem closure_subset_iff_isClosed {α : Type u} [inst : ] {s : Set α} :
s
@[simp]
theorem closure_empty {α : Type u} [inst : ] :
@[simp]
theorem closure_empty_iff {α : Type u} [inst : ] (s : Set α) :
s =
@[simp]
theorem closure_nonempty_iff {α : Type u} [inst : ] {s : Set α} :
theorem Set.Nonempty.closure {α : Type u} [inst : ] {s : Set α} :

Alias of the reverse direction of closure_nonempty_iff.

theorem Set.Nonempty.of_closure {α : Type u} [inst : ] {s : Set α} :

Alias of the forward direction of closure_nonempty_iff.

@[simp]
theorem closure_univ {α : Type u} [inst : ] :
closure Set.univ = Set.univ
@[simp]
theorem closure_closure {α : Type u} [inst : ] {s : Set α} :
@[simp]
theorem closure_union {α : Type u} [inst : ] {s : Set α} {t : Set α} :
closure (s t) =
@[simp]
theorem Finset.closure_bunionᵢ {α : Type u} [inst : ] {ι : Type u_1} (s : ) (f : ιSet α) :
closure (Set.unionᵢ fun i => Set.unionᵢ fun h => f i) = Set.unionᵢ fun i => Set.unionᵢ fun h => closure (f i)
@[simp]
theorem closure_unionᵢ {α : Type u} [inst : ] {ι : Type u_1} [inst : ] (f : ιSet α) :
closure (Set.unionᵢ fun i => f i) = Set.unionᵢ fun i => closure (f i)
theorem interior_subset_closure {α : Type u} [inst : ] {s : Set α} :
theorem closure_eq_compl_interior_compl {α : Type u} [inst : ] {s : Set α} :
@[simp]
theorem interior_compl {α : Type u} [inst : ] {s : Set α} :
@[simp]
theorem closure_compl {α : Type u} [inst : ] {s : Set α} :
theorem mem_closure_iff {α : Type u} [inst : ] {s : Set α} {a : α} :
a ∀ (o : Set α), a oSet.Nonempty (o s)
theorem closure_inter_open_nonempty_iff {α : Type u} [inst : ] {s : Set α} {t : Set α} (h : ) :
theorem Filter.le_lift'_closure {α : Type u} [inst : ] (l : ) :
l Filter.lift' l closure
theorem Filter.HasBasis.lift'_closure {α : Type u} {ι : Sort w} [inst : ] {l : } {p : ιProp} {s : ιSet α} (h : ) :
Filter.HasBasis (Filter.lift' l closure) p fun i => closure (s i)
theorem Filter.HasBasis.lift'_closure_eq_self {α : Type u} {ι : Sort w} [inst : ] {l : } {p : ιProp} {s : ιSet α} (h : ) (hc : ∀ (i : ι), p iIsClosed (s i)) :
Filter.lift' l closure = l
@[simp]
theorem Filter.lift'_closure_eq_bot {α : Type u} [inst : ] {l : } :
Filter.lift' l closure = l =
def Dense {α : Type u} [inst : ] (s : Set α) :

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

Equations
• = ∀ (x : α), x
theorem dense_iff_closure_eq {α : Type u} [inst : ] {s : Set α} :
= Set.univ
theorem Dense.closure_eq {α : Type u} [inst : ] {s : Set α} :
= Set.univ

Alias of the forward direction of dense_iff_closure_eq.

theorem interior_eq_empty_iff_dense_compl {α : Type u} [inst : ] {s : Set α} :
theorem Dense.interior_compl {α : Type u} [inst : ] {s : Set α} (h : ) :
@[simp]
theorem dense_closure {α : Type u} [inst : ] {s : Set α} :

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

theorem Dense.closure {α : Type u} [inst : ] {s : Set α} (h : ) :
theorem Dense.of_closure {α : Type u} [inst : ] {s : Set α} :
Dense ()

Alias of the forward direction of dense_closure.

@[simp]
theorem dense_univ {α : Type u} [inst : ] :
Dense Set.univ
theorem dense_iff_inter_open {α : Type u} [inst : ] {s : Set α} :
∀ (U : Set α), Set.Nonempty (U s)

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

theorem Dense.inter_open_nonempty {α : Type u} [inst : ] {s : Set α} :
∀ (U : Set α), Set.Nonempty (U s)

Alias of the forward direction of dense_iff_inter_open.

theorem Dense.exists_mem_open {α : Type u} [inst : ] {s : Set α} (hs : ) {U : Set α} (ho : ) (hne : ) :
x, x s x U
theorem Dense.nonempty_iff {α : Type u} [inst : ] {s : Set α} (hs : ) :
theorem Dense.nonempty {α : Type u} [inst : ] [h : ] {s : Set α} (hs : ) :
theorem Dense.mono {α : Type u} [inst : ] {s₁ : Set α} {s₂ : Set α} (h : s₁ s₂) (hd : Dense s₁) :
Dense s₂
theorem dense_compl_singleton_iff_not_open {α : Type u} [inst : ] {x : α} :

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

### Frontier of a set #

def frontier {α : Type u} [inst : ] (s : Set α) :
Set α

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

Equations
@[simp]
theorem closure_diff_interior {α : Type u} [inst : ] (s : Set α) :
\ =
@[simp]
theorem closure_diff_frontier {α : Type u} [inst : ] (s : Set α) :
\ =
@[simp]
theorem self_diff_frontier {α : Type u} [inst : ] (s : Set α) :
s \ =
theorem frontier_eq_closure_inter_closure {α : Type u} [inst : ] {s : Set α} :
theorem frontier_subset_closure {α : Type u} [inst : ] {s : Set α} :
theorem IsClosed.frontier_subset {α : Type u} {s : Set α} [inst : ] (hs : ) :
s
theorem frontier_closure_subset {α : Type u} [inst : ] {s : Set α} :
theorem frontier_interior_subset {α : Type u} [inst : ] {s : Set α} :
@[simp]
theorem frontier_compl {α : Type u} [inst : ] (s : Set α) :

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

@[simp]
theorem frontier_univ {α : Type u} [inst : ] :
frontier Set.univ =
@[simp]
theorem frontier_empty {α : Type u} [inst : ] :
theorem frontier_inter_subset {α : Type u} [inst : ] (s : Set α) (t : Set α) :
theorem frontier_union_subset {α : Type u} [inst : ] (s : Set α) (t : Set α) :
theorem IsClosed.frontier_eq {α : Type u} [inst : ] {s : Set α} (hs : ) :
= s \
theorem IsOpen.frontier_eq {α : Type u} [inst : ] {s : Set α} (hs : ) :
= \ s
theorem IsOpen.inter_frontier_eq {α : Type u} [inst : ] {s : Set α} (hs : ) :
theorem isClosed_frontier {α : Type u} [inst : ] {s : Set α} :

The frontier of a set is closed.

theorem interior_frontier {α : Type u} [inst : ] {s : Set α} (h : ) :

The frontier of a closed set has no interior point.

theorem closure_eq_interior_union_frontier {α : Type u} [inst : ] (s : Set α) :
=
theorem closure_eq_self_union_frontier {α : Type u} [inst : ] (s : Set α) :
= s
theorem Disjoint.frontier_left {α : Type u} {s : Set α} {t : Set α} [inst : ] (ht : ) (hd : Disjoint s t) :
theorem Disjoint.frontier_right {α : Type u} {s : Set α} {t : Set α} [inst : ] (hs : ) (hd : Disjoint s t) :
theorem frontier_eq_inter_compl_interior {α : Type u} [inst : ] {s : Set α} :
theorem compl_frontier_eq_union_interior {α : Type u} [inst : ] {s : Set α} :

### Neighborhoods #

def nhds {α : Type u_1} [inst : ] (a : α) :

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

Equations
theorem nhds_def {α : Type u_1} [inst : ] (a : α) :
nhds a = s, h,
def nhdsWithin {α : Type u} [inst : ] (a : α) (s : Set α) :

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

Equations

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

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

Equations
• One or more equations did not get rendered due to their size.

Notation for the filter of punctured neighborhoods of a point.

Equations

Notation for the filter of right neighborhoods of a point.

Equations

Notation for the filter of left neighborhoods of a point.

Equations

Notation for the filter of punctured right neighborhoods of a point.

Equations

Notation for the filter of punctured left neighborhoods of a point.

Equations
theorem nhds_def' {α : Type u} [inst : ] (a : α) :
nhds a = s, _hs, _ha,
theorem nhds_basis_opens {α : Type u} [inst : ] (a : α) :
Filter.HasBasis (nhds a) (fun s => a s ) fun s => s

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

theorem nhds_basis_closeds {α : Type u} [inst : ] (a : α) :
Filter.HasBasis (nhds a) (fun s => ¬a s ) compl
theorem le_nhds_iff {α : Type u} [inst : ] {f : } {a : α} :
f nhds a ∀ (s : Set α), a ss f

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

theorem nhds_le_of_le {α : Type u} [inst : ] {f : } {a : α} {s : Set α} (h : a s) (o : ) (sf : ) :
nhds a f

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

theorem mem_nhds_iff {α : Type u} [inst : ] {a : α} {s : Set α} :
s nhds a t, t s a t
theorem eventually_nhds_iff {α : Type u} [inst : ] {a : α} {p : αProp} :
Filter.Eventually (fun x => p x) (nhds a) t, ((x : α) → x tp x) a t

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

theorem mem_interior_iff_mem_nhds {α : Type u} [inst : ] {s : Set α} {a : α} :
a s nhds a
theorem map_nhds {α : Type u} {β : Type v} [inst : ] {a : α} {f : αβ} :
Filter.map f (nhds a) = s, h, Filter.principal (f '' s)
theorem mem_of_mem_nhds {α : Type u} [inst : ] {a : α} {s : Set α} :
s nhds aa s
theorem Filter.Eventually.self_of_nhds {α : Type u} [inst : ] {p : αProp} {a : α} (h : Filter.Eventually (fun y => p y) (nhds a)) :
p a

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

theorem IsOpen.mem_nhds {α : Type u} [inst : ] {a : α} {s : Set α} (hs : ) (ha : a s) :
s nhds a
theorem IsOpen.mem_nhds_iff {α : Type u} [inst : ] {a : α} {s : Set α} (hs : ) :
s nhds a a s
theorem IsClosed.compl_mem_nhds {α : Type u} [inst : ] {a : α} {s : Set α} (hs : ) (ha : ¬a s) :
theorem IsOpen.eventually_mem {α : Type u} [inst : ] {a : α} {s : Set α} (hs : ) (ha : a s) :
Filter.Eventually (fun x => x s) (nhds a)
theorem nhds_basis_opens' {α : Type u} [inst : ] (a : α) :
Filter.HasBasis (nhds a) (fun s => s nhds a ) fun x => x

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

theorem exists_open_set_nhds {α : Type u} [inst : ] {s : Set α} {U : Set α} (h : ∀ (x : α), x sU nhds x) :
V, s V V U

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

theorem exists_open_set_nhds' {α : Type u} [inst : ] {s : Set α} {U : Set α} (h : U x, h, nhds x) :
V, s V V U

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

theorem Filter.Eventually.eventually_nhds {α : Type u} [inst : ] {p : αProp} {a : α} (h : Filter.Eventually (fun y => p y) (nhds a)) :
Filter.Eventually (fun y => Filter.Eventually (fun x => p x) (nhds y)) (nhds a)

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

@[simp]
theorem eventually_eventually_nhds {α : Type u} [inst : ] {p : αProp} {a : α} :
Filter.Eventually (fun y => Filter.Eventually (fun x => p x) (nhds y)) (nhds a) Filter.Eventually (fun x => p x) (nhds a)
@[simp]
theorem frequently_frequently_nhds {α : Type u} [inst : ] {p : αProp} {a : α} :
Filter.Frequently (fun y => Filter.Frequently (fun x => p x) (nhds y)) (nhds a) Filter.Frequently (fun x => p x) (nhds a)
@[simp]
theorem eventually_mem_nhds {α : Type u} [inst : ] {s : Set α} {a : α} :
Filter.Eventually (fun x => s nhds x) (nhds a) s nhds a
@[simp]
theorem nhds_bind_nhds {α : Type u} {a : α} [inst : ] :
Filter.bind (nhds a) nhds = nhds a
@[simp]
theorem eventually_eventuallyEq_nhds {α : Type u} {β : Type v} [inst : ] {f : αβ} {g : αβ} {a : α} :
Filter.Eventually (fun y => f =ᶠ[nhds y] g) (nhds a) f =ᶠ[nhds a] g
theorem Filter.EventuallyEq.eq_of_nhds {α : Type u} {β : Type v} [inst : ] {f : αβ} {g : αβ} {a : α} (h : f =ᶠ[nhds a] g) :
f a = g a
@[simp]
theorem eventually_eventuallyLE_nhds {α : Type u} {β : Type v} [inst : ] [inst : LE β] {f : αβ} {g : αβ} {a : α} :
theorem Filter.EventuallyEq.eventuallyEq_nhds {α : Type u} {β : Type v} [inst : ] {f : αβ} {g : αβ} {a : α} (h : f =ᶠ[nhds a] g) :
Filter.Eventually (fun y => f =ᶠ[nhds y] g) (nhds a)

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

theorem Filter.EventuallyLE.eventuallyLE_nhds {α : Type u} {β : Type v} [inst : ] [inst : LE β] {f : αβ} {g : αβ} {a : α} (h : f ≤ᶠ[nhds a] g) :
Filter.Eventually (fun y => f ≤ᶠ[nhds y] g) (nhds a)

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

theorem all_mem_nhds {α : Type u} [inst : ] (x : α) (P : Set αProp) (hP : (s t : Set α) → s tP sP t) :
((s : Set α) → s nhds xP s) (s : Set α) → x sP s
theorem all_mem_nhds_filter {α : Type u} {β : Type v} [inst : ] (x : α) (f : Set αSet β) (hf : ∀ (s t : Set α), s tf s f t) (l : ) :
(∀ (s : Set α), s nhds xf s l) ∀ (s : Set α), x sf s l
theorem tendsto_nhds {α : Type u} {β : Type v} [inst : ] {f : βα} {l : } {a : α} :
Filter.Tendsto f l (nhds a) ∀ (s : Set α), a sf ⁻¹' s l
theorem tendsto_atTop_nhds {α : Type u} {β : Type v} [inst : ] [inst : ] [inst : ] {f : βα} {a : α} :
Filter.Tendsto f Filter.atTop (nhds a) ∀ (U : Set α), a UN, ∀ (n : β), N nf n U
theorem tendsto_const_nhds {α : Type u} {β : Type v} [inst : ] {a : α} {f : } :
Filter.Tendsto (fun x => a) f (nhds a)
theorem tendsto_atTop_of_eventually_const {α : Type u} [inst : ] {ι : Type u_1} [inst : ] [inst : ] {x : α} {u : ια} {i₀ : ι} (h : ∀ (i : ι), i i₀u i = x) :
Filter.Tendsto u Filter.atTop (nhds x)
theorem tendsto_atBot_of_eventually_const {α : Type u} [inst : ] {ι : Type u_1} [inst : ] [inst : ] {x : α} {u : ια} {i₀ : ι} (h : ∀ (i : ι), i i₀u i = x) :
Filter.Tendsto u Filter.atBot (nhds x)
theorem pure_le_nhds {α : Type u} [inst : ] :
pure nhds
theorem tendsto_pure_nhds {β : Type v} {α : Type u_1} [inst : ] (f : αβ) (a : α) :
Filter.Tendsto f (pure a) (nhds (f a))
theorem OrderTop.tendsto_atTop_nhds {β : Type v} {α : Type u_1} [inst : ] [inst : ] [inst : ] (f : αβ) :
Filter.Tendsto f Filter.atTop (nhds (f ))
@[simp]
instance nhds_neBot {α : Type u} [inst : ] {a : α} :
Equations

### Cluster points #

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

def ClusterPt {α : Type u} [inst : ] (x : α) (F : ) :

A point x is a cluster point of a filter F if 𝓝 x ⊓ F ≠ ⊥⊓ 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 ≠ ⊥≠] x ⊓ F ≠ ⊥⊓ F ≠ ⊥≠ ⊥⊥. See mem_closure_iff_clusterPt in particular.

Equations
theorem ClusterPt.neBot {α : Type u} [inst : ] {x : α} {F : } (h : ) :
theorem Filter.HasBasis.clusterPt_iff {α : Type u} {a : α} [inst : ] {ιa : Sort u_1} {ιF : Sort u_2} {pa : ιaProp} {sa : ιaSet α} {pF : ιFProp} {sF : ιFSet α} {F : } (ha : Filter.HasBasis (nhds a) pa sa) (hF : Filter.HasBasis F pF sF) :
∀ ⦃i : ιa⦄, pa i∀ ⦃j : ιF⦄, pF jSet.Nonempty (sa i sF j)
theorem clusterPt_iff {α : Type u} [inst : ] {x : α} {F : } :
∀ ⦃U : Set α⦄, U nhds x∀ ⦃V : Set α⦄, V FSet.Nonempty (U V)
theorem clusterPt_iff_not_disjoint {α : Type u} [inst : ] {x : α} {F : } :
theorem clusterPt_principal_iff {α : Type u} [inst : ] {x : α} {s : Set α} :
∀ (U : Set α), U nhds xSet.Nonempty (U s)

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

theorem clusterPt_principal_iff_frequently {α : Type u} [inst : ] {x : α} {s : Set α} :
Filter.Frequently (fun y => y s) (nhds x)
theorem ClusterPt.of_le_nhds {α : Type u} [inst : ] {x : α} {f : } (H : f nhds x) [inst : ] :
theorem ClusterPt.of_le_nhds' {α : Type u} [inst : ] {x : α} {f : } (H : f nhds x) (_hf : ) :
theorem ClusterPt.of_nhds_le {α : Type u} [inst : ] {x : α} {f : } (H : nhds x f) :
theorem ClusterPt.mono {α : Type u} [inst : ] {x : α} {f : } {g : } (H : ) (h : f g) :
theorem ClusterPt.of_inf_left {α : Type u} [inst : ] {x : α} {f : } {g : } (H : ClusterPt x (f g)) :
theorem ClusterPt.of_inf_right {α : Type u} [inst : ] {x : α} {f : } {g : } (H : ClusterPt x (f g)) :
theorem Ultrafilter.clusterPt_iff {α : Type u} [inst : ] {x : α} {f : } :
ClusterPt x f f nhds x
def MapClusterPt {α : Type u} [inst : ] {ι : Type u_1} (x : α) (F : ) (u : ια) :

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

Equations
theorem mapClusterPt_iff {α : Type u} [inst : ] {ι : Type u_1} (x : α) (F : ) (u : ια) :
MapClusterPt x F u ∀ (s : Set α), s nhds xFilter.Frequently (fun a => u a s) F
theorem mapClusterPt_of_comp {α : Type u} [inst : ] {ι : Type u_1} {δ : Type u_2} {F : } {φ : δι} {p : } {x : α} {u : ια} [inst : ] (h : ) (H : Filter.Tendsto (u φ) p (nhds x)) :
def AccPt {α : Type u} [inst : ] (x : α) (F : ) :

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

Equations
theorem acc_iff_cluster {α : Type u} [inst : ] (x : α) (F : ) :
theorem acc_principal_iff_cluster {α : Type u} [inst : ] (x : α) (C : Set α) :

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

theorem accPt_iff_nhds {α : Type u} [inst : ] (x : α) (C : Set α) :
∀ (U : Set α), U nhds xy, y U C y x

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

theorem accPt_iff_frequently {α : Type u} [inst : ] (x : α) (C : Set α) :
Filter.Frequently (fun y => y x y C) (nhds x)

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

theorem AccPt.mono {α : Type u} [inst : ] {x : α} {F : } {G : } (h : AccPt x F) (hFG : F G) :
AccPt x G

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

### Interior, closure and frontier in terms of neighborhoods #

theorem interior_eq_nhds' {α : Type u} [inst : ] {s : Set α} :
= { a | s nhds a }
theorem interior_eq_nhds {α : Type u} [inst : ] {s : Set α} :
= { a | }
@[simp]
theorem interior_mem_nhds {α : Type u} [inst : ] {s : Set α} {a : α} :
theorem interior_setOf_eq {α : Type u} [inst : ] {p : αProp} :
interior { x | p x } = { x | Filter.Eventually (fun y => p y) (nhds x) }
theorem isOpen_setOf_eventually_nhds {α : Type u} [inst : ] {p : αProp} :
IsOpen { x | Filter.Eventually (fun y => p y) (nhds x) }
theorem subset_interior_iff_nhds {α : Type u} [inst : ] {s : Set α} {V : Set α} :
s ∀ (x : α), x sV nhds x
theorem isOpen_iff_nhds {α : Type u} [inst : ] {s : Set α} :
∀ (a : α), a s
theorem isOpen_iff_mem_nhds {α : Type u} [inst : ] {s : Set α} :
∀ (a : α), a ss nhds a
theorem isOpen_iff_eventually {α : Type u} [inst : ] {s : Set α} :
∀ (x : α), x sFilter.Eventually (fun y => y s) (nhds x)

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

theorem isOpen_iff_ultrafilter {α : Type u} [inst : ] {s : Set α} :
∀ (x : α), x s∀ (l : ), l nhds xs l
theorem isOpen_singleton_iff_nhds_eq_pure {α : Type u} [inst : ] (a : α) :
IsOpen {a} nhds a = pure a
theorem isOpen_singleton_iff_punctured_nhds {α : Type u_1} [inst : ] (a : α) :
theorem mem_closure_iff_frequently {α : Type u} [inst : ] {s : Set α} {a : α} :
a Filter.Frequently (fun x => x s) (nhds a)
theorem Filter.Frequently.mem_closure {α : Type u} [inst : ] {s : Set α} {a : α} :
Filter.Frequently (fun x => x s) (nhds a)a

Alias of the reverse direction of mem_closure_iff_frequently.

theorem isClosed_iff_frequently {α : Type u} [inst : ] {s : Set α} :
∀ (x : α), Filter.Frequently (fun y => y s) (nhds x)x s

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

theorem isClosed_setOf_clusterPt {α : Type u} [inst : ] {f : } :
IsClosed { x | }

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

theorem mem_closure_iff_clusterPt {α : Type u} [inst : ] {s : Set α} {a : α} :
a
theorem mem_closure_iff_nhds_neBot {α : Type u} {a : α} [inst : ] {s : Set α} :
theorem mem_closure_iff_nhdsWithin_neBot {α : Type u} [inst : ] {s : Set α} {x : α} :
theorem dense_compl_singleton {α : Type u} [inst : ] (x : α) [inst : Filter.NeBot (nhdsWithin x ({x}))] :
Dense ({x})

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

theorem closure_compl_singleton {α : Type u} [inst : ] (x : α) [inst : Filter.NeBot (nhdsWithin x ({x}))] :
closure ({x}) = Set.univ

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

@[simp]
theorem interior_singleton {α : Type u} [inst : ] (x : α) [inst : Filter.NeBot (nhdsWithin x ({x}))] :

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

theorem not_isOpen_singleton {α : Type u} [inst : ] (x : α) [inst : Filter.NeBot (nhdsWithin x ({x}))] :
theorem closure_eq_cluster_pts {α : Type u} [inst : ] {s : Set α} :
= { a | }
theorem mem_closure_iff_nhds {α : Type u} [inst : ] {s : Set α} {a : α} :
a ∀ (t : Set α), t nhds aSet.Nonempty (t s)
theorem mem_closure_iff_nhds' {α : Type u} [inst : ] {s : Set α} {a : α} :
a ∀ (t : Set α), t nhds ay, y t
theorem mem_closure_iff_comap_neBot {α : Type u} [inst : ] {A : Set α} {x : α} :
x Filter.NeBot (Filter.comap Subtype.val (nhds x))
theorem mem_closure_iff_nhds_basis' {α : Type u} {ι : Sort w} [inst : ] {a : α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis (nhds a) p s) {t : Set α} :
a ∀ (i : ι), p iSet.Nonempty (s i t)
theorem mem_closure_iff_nhds_basis {α : Type u} {ι : Sort w} [inst : ] {a : α} {p : ιProp} {s : ιSet α} (h : Filter.HasBasis (nhds a) p s) {t : Set α} :
a ∀ (i : ι), p iy, y t y s i
theorem mem_closure_iff_ultrafilter {α : Type u} [inst : ] {s : Set α} {x : α} :
x u, s u u nhds x

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

theorem isClosed_iff_clusterPt {α : Type u} [inst : ] {s : Set α} :
∀ (a : α), a s
theorem isClosed_iff_nhds {α : Type u} [inst : ] {s : Set α} :
∀ (x : α), (∀ (U : Set α), U nhds xSet.Nonempty (U s)) → x s
theorem IsClosed.interior_union_left {α : Type u} [inst : ] {s : Set α} {t : Set α} :
interior (s t) s
theorem IsClosed.interior_union_right {α : Type u} [inst : ] {s : Set α} {t : Set α} (h : ) :
theorem IsOpen.inter_closure {α : Type u} [inst : ] {s : Set α} {t : Set α} (h : ) :
s closure (s t)
theorem IsOpen.closure_inter {α : Type u} [inst : ] {s : Set α} {t : Set α} (h : ) :
t closure (s t)
theorem Dense.open_subset_closure_inter {α : Type u} [inst : ] {s : Set α} {t : Set α} (hs : ) (ht : ) :
t closure (t s)
theorem mem_closure_of_mem_closure_union {α : Type u} [inst : ] {s₁ : Set α} {s₂ : Set α} {x : α} (h : x closure (s₁ s₂)) (h₁ : s₁ nhds x) :
x closure s₂
theorem Dense.inter_of_open_left {α : Type u} [inst : ] {s : Set α} {t : Set α} (hs : ) (ht : ) (hso : ) :
Dense (s t)

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

theorem Dense.inter_of_open_right {α : Type u} [inst : ] {s : Set α} {t : Set α} (hs : ) (ht : ) (hto : ) :
Dense (s t)

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

theorem Dense.inter_nhds_nonempty {α : Type u} [inst : ] {s : Set α} {t : Set α} (hs : ) {x : α} (ht : t nhds x) :
theorem closure_diff {α : Type u} [inst : ] {s : Set α} {t : Set α} :
\ closure (s \ t)
theorem Filter.Frequently.mem_of_closed {α : Type u} [inst : ] {a : α} {s : Set α} (h : Filter.Frequently (fun x => x s) (nhds a)) (hs : ) :
a s
theorem IsClosed.mem_of_frequently_of_tendsto {α : Type u} {β : Type v} [inst : ] {f : βα} {b : } {a : α} {s : Set α} (hs : ) (h : Filter.Frequently (fun x => f x s) b) (hf : Filter.Tendsto f b (nhds a)) :
a s
theorem IsClosed.mem_of_tendsto {α : Type u} {β : Type v} [inst : ] {f : βα} {b : } {a : α} {s : Set α} [inst : ] (hs : ) (hf : Filter.Tendsto f b (nhds a)) (h : Filter.Eventually (fun x => f x s) b) :
a s
theorem mem_closure_of_frequently_of_tendsto {α : Type u} {β : Type v} [inst : ] {f : βα} {b : } {a : α} {s : Set α} (h : Filter.Frequently (fun x => f x s) b) (hf : Filter.Tendsto f b (nhds a)) :
a
theorem mem_closure_of_tendsto {α : Type u} {β : Type v} [inst : ] {f : βα} {b : } {a : α} {s : Set α} [inst : ] (hf : Filter.Tendsto f b (nhds a)) (h : Filter.Eventually (fun x => f x s) b) :
a
theorem tendsto_inf_principal_nhds_iff_of_forall_eq {α : Type u} {β : Type v} [inst : ] {f : βα} {l : } {s : Set β} {a : α} (h : ∀ (x : β), ¬x sf x = a) :

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

### Limits of filters in topological spaces #

In this section we define functions that return a limit of a filter (or of a function along a filter), if it exists, and a random point otherwise. This functions are rarely used in Mathlib, most of the theorems are written using Filter.Tendsto. One of the reasons is that Filter.limUnder f g = a is not equivalent to Filter.Tendsto g f (𝓝 a) unless the codomain is a Hausdorff space and g has a limit along f.

noncomputable def lim {α : Type u} [inst : ] [inst : ] (f : ) :
α

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

Equations
noncomputable def Ultrafilter.lim {α : Type u} [inst : ] (F : ) :
α

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 : Filter.Ultrafilter α.

Equations
noncomputable def limUnder {α : Type u} {β : Type v} [inst : ] [inst : ] (f : ) (g : βα) :
α

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

Equations
theorem le_nhds_lim {α : Type u} [inst : ] {f : } (h : a, f nhds a) :
f nhds (lim f)

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

theorem tendsto_nhds_limUnder {α : Type u} {β : Type v} [inst : ] {f : } {g : βα} (h : a, Filter.Tendsto g f (nhds a)) :

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

### Continuity #

structure Continuous {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) :
• The preimage of an open set under a continuous function is an open set. Use IsOpen.preimage instead.

isOpen_preimage : ∀ (s : Set β), IsOpen (f ⁻¹' s)

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.

Instances For

Notation for Continuous with respect to a non-standard topologies.

Equations
• One or more equations did not get rendered due to their size.
theorem continuous_def {α : Type u_1} {β : Type u_2} :
∀ {x : } {x_1 : } {f : αβ}, ∀ (s : Set β), IsOpen (f ⁻¹' s)
theorem IsOpen.preimage {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} (hf : ) {s : Set β} (h : ) :
theorem Continuous.congr {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {g : αβ} (h : ) (h' : ∀ (x : α), f x = g x) :
def ContinuousAt {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] (f : αβ) (x : α) :

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

Equations
theorem ContinuousAt.tendsto {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {x : α} (h : ) :
Filter.Tendsto f (nhds x) (nhds (f x))
theorem continuousAt_def {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {x : α} :
∀ (A : Set β), A nhds (f x)f ⁻¹' A nhds x
theorem continuousAt_congr {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {g : αβ} {x : α} (h : f =ᶠ[nhds x] g) :
theorem ContinuousAt.congr {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {g : αβ} {x : α} (hf : ) (h : f =ᶠ[nhds x] g) :
theorem ContinuousAt.preimage_mem_nhds {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] {f : αβ} {x : α} {t : Set β} (h : ) (ht : t nhds (f x)) :
theorem eventuallyEq_zero_nhds {α : Type u_2} [inst : ] {M₀ : Type u_1} [inst : Zero M₀] {a : α} {f : αM₀} :
theorem ClusterPt.map {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {x : α} {la : } {lb : } (H : ClusterPt x la) {f : αβ} (hfc : ) (hf : Filter.Tendsto f la lb) :
ClusterPt (f x) lb
theorem preimage_interior_subset_interior_preimage {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] {f : αβ} {s : Set β} (hf : ) :

See also interior_preimage_subset_preimage_interior.

theorem continuous_id {α : Type u_1} [inst : ] :
theorem continuous_id' {α : Type u_1} [inst : ] :
Continuous fun x => x
theorem Continuous.comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : ] [inst : ] [inst : ] {g : βγ} {f : αβ} (hg : ) (hf : ) :
theorem Continuous.comp' {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : ] [inst : ] [inst : ] {g : βγ} {f : αβ} (hg : ) (hf : ) :
Continuous fun x => g (f x)
theorem Continuous.iterate {α : Type u_1} [inst : ] {f : αα} (h : ) (n : ) :
theorem ContinuousAt.comp {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : ] [inst : ] [inst : ] {g : βγ} {f : αβ} {x : α} (hg : ContinuousAt g (f x)) (hf : ) :
theorem Continuous.tendsto {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} (hf : ) (x : α) :
Filter.Tendsto f (nhds x) (nhds (f x))
theorem Continuous.tendsto' {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} (hf : ) (x : α) (y : β) (h : f x = y) :

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

theorem Continuous.continuousAt {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {x : α} (h : ) :
theorem continuous_iff_continuousAt {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} :
∀ (x : α),
theorem continuousAt_const {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {x : α} {b : β} :
ContinuousAt (fun x => b) x
theorem continuous_const {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {b : β} :
Continuous fun x => b
theorem Filter.EventuallyEq.continuousAt {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {x : α} {f : αβ} {y : β} (h : f =ᶠ[nhds x] fun x => y) :
theorem continuous_of_const {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] {f : αβ} (h : ∀ (x y : α), f x = f y) :
theorem continuousAt_id {α : Type u_1} [inst : ] {x : α} :
theorem ContinuousAt.iterate {α : Type u_1} [inst : ] {f : αα} {x : α} (hf : ) (hx : f x = x) (n : ) :
theorem continuous_iff_isClosed {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} :
∀ (s : Set β), IsClosed (f ⁻¹' s)
theorem IsClosed.preimage {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} (hf : ) {s : Set β} (h : ) :
theorem mem_closure_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {x : α} {s : Set α} (hf : ) (hx : x ) :
f x closure (f '' s)
theorem continuousAt_iff_ultrafilter {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {x : α} :
∀ (g : ), g nhds xFilter.Tendsto f (g) (nhds (f x))
theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} :
∀ (x : α) (g : ), g nhds xFilter.Tendsto f (g) (nhds (f x))
theorem Continuous.closure_preimage_subset {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} (hf : ) (t : Set β) :
theorem Continuous.frontier_preimage_subset {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} (hf : ) (t : Set β) :
theorem Set.MapsTo.closure {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) (hc : ) :
Set.MapsTo f () ()

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

theorem image_closure_subset_closure_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {s : Set α} (h : ) :
f '' closure (f '' s)
theorem closure_image_closure {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {s : Set α} (h : ) :
closure (f '' ) = closure (f '' s)
theorem closure_subset_preimage_closure_image {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} {s : Set α} (h : ) :
f ⁻¹' closure (f '' s)
theorem map_mem_closure {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {s : Set α} {t : Set β} {f : αβ} {a : α} (hf : ) (ha : a ) (ht : Set.MapsTo f s t) :
f a
theorem Set.MapsTo.closure_left {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {s : Set α} {t : Set β} {f : αβ} (h : Set.MapsTo f s t) (hc : ) (ht : ) :
Set.MapsTo f () t

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

### Function with dense range #

def DenseRange {β : Type u_1} [inst : ] {κ : Type u_2} (f : κβ) :

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

Equations
theorem Function.Surjective.denseRange {β : Type u_2} [inst : ] {κ : Type u_1} {f : κβ} (hf : ) :

A surjective map has dense range.

theorem denseRange_id {α : Type u_1} [inst : ] :
theorem denseRange_iff_closure_range {β : Type u_1} [inst : ] {κ : Type u_2} {f : κβ} :
closure () = Set.univ
theorem DenseRange.closure_range {β : Type u_1} [inst : ] {κ : Type u_2} {f : κβ} (h : ) :
closure () = Set.univ
theorem Dense.denseRange_val {α : Type u_1} [inst : ] {s : Set α} (h : ) :
DenseRange Subtype.val
theorem Continuous.range_subset_closure_image_dense {α : Type u_1} {β : Type u_2} [inst : ] [inst : ] {f : αβ} (hf : ) {s : Set α} (hs : ) :
closure (f '' s)
theorem DenseRange.dense_image {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] {f : αβ} (hf' : ) (hf : ) {s : Set α} (hs : ) :
Dense (f '' s)

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

theorem DenseRange.subset_closure_image_preimage_of_isOpen {β : Type u_1} [inst : ] {κ : Type u_2} {f : κβ} (hf : ) {s : Set β} (hs : ) :
s closure (f '' (f ⁻¹' s))

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

theorem DenseRange.dense_of_mapsTo {α : Type u_2} {β : Type u_1} [inst : ] [inst : ] {f : αβ} (hf' : ) (hf : ) {s : Set α} (hs : ) {t : Set β} (ht : Set.MapsTo f s t) :

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

theorem DenseRange.comp {β : Type u_2} {γ : Type u_1} [inst : ] [inst : ] {κ : Type u_3} {g : βγ} {f : κβ} (hg : ) (hf : ) (cg : ) :

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

theorem DenseRange.nonempty_iff {β : Type u_1} [inst : ] {κ : Type u_2} {f : κβ} (hf : ) :
theorem DenseRange.nonempty {β : Type u_1} [inst : ] {κ : Type u_2} {f : κβ} [h : ] (hf : ) :
def DenseRange.some {β : Type u_1} [inst : ] {κ : Type u_2} {f : κβ} (hf : ) (b : β) :
κ

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

Equations
theorem DenseRange.exists_mem_open {β : Type u_1} [inst : ] {κ : Type u_2} {f : κβ} (hf : ) {s : Set β} (ho : ) (hs : ) :
a, f a s
theorem DenseRange.mem_nhds {β : Type u_1} [inst : ] {κ : Type u_2} {f : κβ} (h : ) {b : β} {U : Set β} (U_in : U nhds b) :
a, f a U