# Basic theory of topological spaces. #

The main definition is the type class TopologicalSpace X which endows a type X with a topology. Then Set X gets predicates IsOpen, IsClosed and functions interior, closure and frontier. Each point x of X gets a neighborhood filter 𝓝 x. A filter F on X has x as a cluster point if ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥. A map f : α → X 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 X and Y, a function f : X → Y and a point x : X, ContinuousAt f x means f is continuous at x, and global continuity is Continuous f. There is also a version of continuity PContinuous for partially defined functions.

## Notation #

The following notation is introduced elsewhere and it heavily used in this file.

• 𝓝 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: 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 #

def TopologicalSpace.ofClosed {X : Type u} (T : Set (Set X)) (empty_mem : T) (sInter_mem : AT, ⋂₀ A T) (union_mem : AT, BT, A B T) :

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

Equations
Instances For
theorem isOpen_mk {X : Type u} {s : Set X} {p : Set XProp} {h₁ : p Set.univ} {h₂ : ∀ (s t : Set X), p sp tp (s t)} {h₃ : ∀ (s : Set (Set X)), (ts, p t)p (⋃₀ s)} :
p s
theorem TopologicalSpace.ext {X : Type u} {f : } {g : } :
IsOpen = IsOpenf = g
theorem TopologicalSpace.ext_iff {X : Type u} {t : } {t' : } :
t = t' ∀ (s : Set X),
theorem isOpen_fold {X : Type u} {s : Set X} {t : } :
theorem isOpen_iUnion {X : Type u} {ι : Sort w} [] {f : ιSet X} (h : ∀ (i : ι), IsOpen (f i)) :
IsOpen (⋃ (i : ι), f i)
theorem isOpen_biUnion {X : Type u} {α : Type u_1} [] {s : Set α} {f : αSet X} (h : is, IsOpen (f i)) :
IsOpen (is, f i)
theorem IsOpen.union {X : Type u} {s₁ : Set X} {s₂ : Set X} [] (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) :
IsOpen (s₁ s₂)
theorem isOpen_iff_of_cover {X : Type u} {α : Type u_1} {s : Set X} [] {f : αSet X} (ho : ∀ (i : α), IsOpen (f i)) (hU : ⋃ (i : α), f i = Set.univ) :
∀ (i : α), IsOpen (f i s)
@[simp]
theorem isOpen_empty {X : Type u} [] :
theorem Set.Finite.isOpen_sInter {X : Type u} [] {s : Set (Set X)} (hs : s.Finite) :
(ts, )IsOpen (⋂₀ s)
theorem Set.Finite.isOpen_biInter {X : Type u} {α : Type u_1} [] {s : Set α} {f : αSet X} (hs : s.Finite) (h : is, IsOpen (f i)) :
IsOpen (is, f i)
theorem isOpen_iInter_of_finite {X : Type u} {ι : Sort w} [] [] {s : ιSet X} (h : ∀ (i : ι), IsOpen (s i)) :
IsOpen (⋂ (i : ι), s i)
theorem isOpen_biInter_finset {X : Type u} {α : Type u_1} [] {s : } {f : αSet X} (h : is, IsOpen (f i)) :
IsOpen (is, f i)
@[simp]
theorem isOpen_const {X : Type u} [] {p : Prop} :
IsOpen {_x : X | p}
theorem IsOpen.and {X : Type u} {p₁ : XProp} {p₂ : XProp} [] :
IsOpen {x : X | p₁ x}IsOpen {x : X | p₂ x}IsOpen {x : X | p₁ x p₂ x}
@[simp]
theorem isOpen_compl_iff {X : Type u} {s : Set X} [] :
theorem TopologicalSpace.ext_iff_isClosed {X : Type u} {t₁ : } {t₂ : } :
t₁ = t₂ ∀ (s : Set X),
theorem TopologicalSpace.ext_isClosed {X : Type u} {t₁ : } {t₂ : } :
(∀ (s : Set X), )t₁ = t₂

Alias of the reverse direction of TopologicalSpace.ext_iff_isClosed.

theorem isClosed_const {X : Type u} [] {p : Prop} :
IsClosed {_x : X | p}
@[simp]
theorem isClosed_empty {X : Type u} [] :
@[simp]
theorem isClosed_univ {X : Type u} [] :
IsClosed Set.univ
theorem IsClosed.union {X : Type u} {s₁ : Set X} {s₂ : Set X} [] :
IsClosed s₁IsClosed s₂IsClosed (s₁ s₂)
theorem isClosed_sInter {X : Type u} [] {s : Set (Set X)} :
(ts, )IsClosed (⋂₀ s)
theorem isClosed_iInter {X : Type u} {ι : Sort w} [] {f : ιSet X} (h : ∀ (i : ι), IsClosed (f i)) :
IsClosed (⋂ (i : ι), f i)
theorem isClosed_biInter {X : Type u} {α : Type u_1} [] {s : Set α} {f : αSet X} (h : is, IsClosed (f i)) :
IsClosed (is, f i)
@[simp]
theorem isClosed_compl_iff {X : Type u} [] {s : Set X} :
theorem IsOpen.isClosed_compl {X : Type u} [] {s : Set X} :

Alias of the reverse direction of isClosed_compl_iff.

theorem IsOpen.sdiff {X : Type u} {s : Set X} {t : Set X} [] (h₁ : ) (h₂ : ) :
IsOpen (s \ t)
theorem IsClosed.inter {X : Type u} {s₁ : Set X} {s₂ : Set X} [] (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) :
IsClosed (s₁ s₂)
theorem IsClosed.sdiff {X : Type u} {s : Set X} {t : Set X} [] (h₁ : ) (h₂ : ) :
IsClosed (s \ t)
theorem Set.Finite.isClosed_biUnion {X : Type u} {α : Type u_1} [] {s : Set α} {f : αSet X} (hs : s.Finite) (h : is, IsClosed (f i)) :
IsClosed (is, f i)
theorem isClosed_biUnion_finset {X : Type u} {α : Type u_1} [] {s : } {f : αSet X} (h : is, IsClosed (f i)) :
IsClosed (is, f i)
theorem isClosed_iUnion_of_finite {X : Type u} {ι : Sort w} [] [] {s : ιSet X} (h : ∀ (i : ι), IsClosed (s i)) :
IsClosed (⋃ (i : ι), s i)
theorem isClosed_imp {X : Type u} [] {p : XProp} {q : XProp} (hp : IsOpen {x : X | p x}) (hq : IsClosed {x : X | q x}) :
IsClosed {x : X | p xq x}
theorem IsClosed.not {X : Type u} {p : XProp} [] :
IsClosed {a : X | p a}IsOpen {a : X | ¬p a}

### Interior of a set #

theorem mem_interior {X : Type u} {x : X} {s : Set X} [] :
x ts, x t
@[simp]
theorem isOpen_interior {X : Type u} {s : Set X} [] :
theorem interior_subset {X : Type u} {s : Set X} [] :
s
theorem interior_maximal {X : Type u} {s : Set X} {t : Set X} [] (h₁ : t s) (h₂ : ) :
t
theorem IsOpen.interior_eq {X : Type u} {s : Set X} [] (h : ) :
= s
theorem interior_eq_iff_isOpen {X : Type u} {s : Set X} [] :
= s
theorem subset_interior_iff_isOpen {X : Type u} {s : Set X} [] :
s
theorem IsOpen.subset_interior_iff {X : Type u} {s : Set X} {t : Set X} [] (h₁ : ) :
s s t
theorem subset_interior_iff {X : Type u} {s : Set X} {t : Set X} [] :
t ∃ (U : Set X), t U U s
theorem interior_subset_iff {X : Type u} {s : Set X} {t : Set X} [] :
t ∀ (U : Set X), U sU t
theorem interior_mono {X : Type u} {s : Set X} {t : Set X} [] (h : s t) :
@[simp]
theorem interior_empty {X : Type u} [] :
@[simp]
theorem interior_univ {X : Type u} [] :
interior Set.univ = Set.univ
@[simp]
theorem interior_eq_univ {X : Type u} {s : Set X} [] :
= Set.univ s = Set.univ
@[simp]
theorem interior_interior {X : Type u} {s : Set X} [] :
@[simp]
theorem interior_inter {X : Type u} {s : Set X} {t : Set X} [] :
interior (s t) =
theorem Set.Finite.interior_biInter {X : Type u} [] {ι : Type u_3} {s : Set ι} (hs : s.Finite) (f : ιSet X) :
interior (is, f i) = is, interior (f i)
theorem Set.Finite.interior_sInter {X : Type u} [] {S : Set (Set X)} (hS : S.Finite) :
interior (⋂₀ S) = sS,
@[simp]
theorem Finset.interior_iInter {X : Type u} [] {ι : Type u_3} (s : ) (f : ιSet X) :
interior (is, f i) = is, interior (f i)
@[simp]
theorem interior_iInter_of_finite {X : Type u} {ι : Sort w} [] [] (f : ιSet X) :
interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
@[simp]
theorem interior_iInter₂_lt_nat {X : Type u} [] {n : } (f : Set X) :
interior (⋂ (m : ), ⋂ (_ : m < n), f m) = ⋂ (m : ), ⋂ (_ : m < n), interior (f m)
@[simp]
theorem interior_iInter₂_le_nat {X : Type u} [] {n : } (f : Set X) :
interior (⋂ (m : ), ⋂ (_ : m n), f m) = ⋂ (m : ), ⋂ (_ : m n), interior (f m)
theorem interior_union_isClosed_of_interior_empty {X : Type u} {s : Set X} {t : Set X} [] (h₁ : ) (h₂ : ) :
interior (s t) =
theorem isOpen_iff_forall_mem_open {X : Type u} {s : Set X} [] :
xs, ts, x t
theorem interior_iInter_subset {X : Type u} {ι : Sort w} [] (s : ιSet X) :
interior (⋂ (i : ι), s i) ⋂ (i : ι), interior (s i)
theorem interior_iInter₂_subset {X : Type u} {ι : Sort w} [] (p : ιSort u_3) (s : (i : ι) → p iSet X) :
interior (⋂ (i : ι), ⋂ (j : p i), s i j) ⋂ (i : ι), ⋂ (j : p i), interior (s i j)
theorem interior_sInter_subset {X : Type u} [] (S : Set (Set X)) :
interior (⋂₀ S) sS,
theorem Filter.HasBasis.lift'_interior {X : Type u} {ι : Sort w} [] {l : } {p : ιProp} {s : ιSet X} (h : l.HasBasis p s) :
(l.lift' interior).HasBasis p fun (i : ι) => interior (s i)
theorem Filter.lift'_interior_le {X : Type u} [] (l : ) :
l.lift' interior l
theorem Filter.HasBasis.lift'_interior_eq_self {X : Type u} {ι : Sort w} [] {l : } {p : ιProp} {s : ιSet X} (h : l.HasBasis p s) (ho : ∀ (i : ι), p iIsOpen (s i)) :
l.lift' interior = l

### Closure of a set #

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

Alias of the reverse direction of closure_nonempty_iff.

theorem Set.Nonempty.of_closure {X : Type u} {s : Set X} [] :
().Nonemptys.Nonempty

Alias of the forward direction of closure_nonempty_iff.

@[simp]
theorem closure_univ {X : Type u} [] :
closure Set.univ = Set.univ
@[simp]
theorem closure_closure {X : Type u} {s : Set X} [] :
theorem closure_eq_compl_interior_compl {X : Type u} {s : Set X} [] :
= ()
@[simp]
theorem closure_union {X : Type u} {s : Set X} {t : Set X} [] :
closure (s t) =
theorem Set.Finite.closure_biUnion {X : Type u} [] {ι : Type u_3} {s : Set ι} (hs : s.Finite) (f : ιSet X) :
closure (is, f i) = is, closure (f i)
theorem Set.Finite.closure_sUnion {X : Type u} [] {S : Set (Set X)} (hS : S.Finite) :
closure (⋃₀ S) = sS,
@[simp]
theorem Finset.closure_biUnion {X : Type u} [] {ι : Type u_3} (s : ) (f : ιSet X) :
closure (is, f i) = is, closure (f i)
@[simp]
theorem closure_iUnion_of_finite {X : Type u} {ι : Sort w} [] [] (f : ιSet X) :
closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
@[simp]
theorem closure_iUnion₂_lt_nat {X : Type u} [] {n : } (f : Set X) :
closure (⋃ (m : ), ⋃ (_ : m < n), f m) = ⋃ (m : ), ⋃ (_ : m < n), closure (f m)
@[simp]
theorem closure_iUnion₂_le_nat {X : Type u} [] {n : } (f : Set X) :
closure (⋃ (m : ), ⋃ (_ : m n), f m) = ⋃ (m : ), ⋃ (_ : m n), closure (f m)
theorem interior_subset_closure {X : Type u} {s : Set X} [] :
@[simp]
theorem interior_compl {X : Type u} {s : Set X} [] :
= ()
@[simp]
theorem closure_compl {X : Type u} {s : Set X} [] :
= ()
theorem mem_closure_iff {X : Type u} {x : X} {s : Set X} [] :
x ∀ (o : Set X), x o(o s).Nonempty
theorem closure_inter_open_nonempty_iff {X : Type u} {s : Set X} {t : Set X} [] (h : ) :
( t).Nonempty (s t).Nonempty
theorem Filter.le_lift'_closure {X : Type u} [] (l : ) :
l l.lift' closure
theorem Filter.HasBasis.lift'_closure {X : Type u} {ι : Sort w} [] {l : } {p : ιProp} {s : ιSet X} (h : l.HasBasis p s) :
(l.lift' closure).HasBasis p fun (i : ι) => closure (s i)
theorem Filter.HasBasis.lift'_closure_eq_self {X : Type u} {ι : Sort w} [] {l : } {p : ιProp} {s : ιSet X} (h : l.HasBasis p s) (hc : ∀ (i : ι), p iIsClosed (s i)) :
l.lift' closure = l
@[simp]
theorem Filter.lift'_closure_eq_bot {X : Type u} [] {l : } :
l.lift' closure = l =
theorem dense_iff_closure_eq {X : Type u} {s : Set X} [] :
= Set.univ
theorem Dense.closure_eq {X : Type u} {s : Set X} [] :
= Set.univ

Alias of the forward direction of dense_iff_closure_eq.

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

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

theorem Dense.closure {X : Type u} {s : Set X} [] :
Dense ()

Alias of the reverse direction of dense_closure.

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

theorem Dense.of_closure {X : Type u} {s : Set X} [] :
Dense ()

Alias of the forward direction of dense_closure.

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

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

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

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

Alias of the forward direction of dense_iff_inter_open.

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

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

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

### Frontier of a set #

@[simp]
theorem closure_diff_interior {X : Type u} [] (s : Set X) :
\ =
theorem disjoint_interior_frontier {X : Type u} {s : Set X} [] :
Disjoint () ()

Interior and frontier are disjoint.

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

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

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

The frontier of a set is closed.

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

The frontier of a closed set has no interior point.

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

### Neighborhoods #

theorem nhds_def' {X : Type u} [] (x : X) :
nhds x = ⨅ (s : Set X), ⨅ (_ : ), ⨅ (_ : x s),
theorem nhds_basis_opens {X : Type u} [] (x : X) :
(nhds x).HasBasis (fun (s : Set X) => x s ) fun (s : Set X) => s

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

theorem nhds_basis_closeds {X : Type u} [] (x : X) :
(nhds x).HasBasis (fun (s : Set X) => xs ) compl
@[simp]
theorem lift'_nhds_interior {X : Type u} [] (x : X) :
(nhds x).lift' interior = nhds x
theorem Filter.HasBasis.nhds_interior {X : Type u} {ι : Sort w} [] {x : X} {p : ιProp} {s : ιSet X} (h : (nhds x).HasBasis p s) :
(nhds x).HasBasis p fun (x : ι) => interior (s x)
theorem le_nhds_iff {X : Type u} {x : X} [] {f : } :
f nhds x ∀ (s : Set X), x ss f

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

theorem nhds_le_of_le {X : Type u} {x : X} {s : Set X} [] {f : } (h : x s) (o : ) (sf : ) :
nhds x f

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

theorem mem_nhds_iff {X : Type u} {x : X} {s : Set X} [] :
s nhds x ts, x t
theorem eventually_nhds_iff {X : Type u} {x : X} [] {p : XProp} :
(∀ᶠ (x : X) in nhds x, p x) ∃ (t : Set X), (xt, p x) x t

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

theorem mem_interior_iff_mem_nhds {X : Type u} {x : X} {s : Set X} [] :
x s nhds x
theorem map_nhds {X : Type u} {α : Type u_1} {x : X} [] {f : Xα} :
Filter.map f (nhds x) = s{s : Set X | x s }, Filter.principal (f '' s)
theorem mem_of_mem_nhds {X : Type u} {x : X} {s : Set X} [] :
s nhds xx s
theorem Filter.Eventually.self_of_nhds {X : Type u} {x : X} [] {p : XProp} (h : ∀ᶠ (y : X) in nhds x, p y) :
p x

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

theorem IsOpen.mem_nhds {X : Type u} {x : X} {s : Set X} [] (hs : ) (hx : x s) :
s nhds x
theorem IsOpen.mem_nhds_iff {X : Type u} {x : X} {s : Set X} [] (hs : ) :
s nhds x x s
theorem IsClosed.compl_mem_nhds {X : Type u} {x : X} {s : Set X} [] (hs : ) (hx : xs) :
theorem IsOpen.eventually_mem {X : Type u} {x : X} {s : Set X} [] (hs : ) (hx : x s) :
∀ᶠ (x : X) in nhds x, x s
theorem nhds_basis_opens' {X : Type u} [] (x : X) :
(nhds x).HasBasis (fun (s : Set X) => s nhds x ) fun (x : Set X) => x

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

theorem exists_open_set_nhds {X : Type u} {s : Set X} [] {U : Set X} (h : xs, U nhds x) :
∃ (V : Set X), 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' {X : Type u} {s : Set X} [] {U : Set X} (h : U xs, nhds x) :
∃ (V : Set X), 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 {X : Type u} {x : X} [] {p : XProp} (h : ∀ᶠ (y : X) in nhds x, p y) :
∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x

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

@[simp]
theorem eventually_eventually_nhds {X : Type u} {x : X} [] {p : XProp} :
(∀ᶠ (y : X) in nhds x, ∀ᶠ (x : X) in nhds y, p x) ∀ᶠ (x : X) in nhds x, p x
@[simp]
theorem frequently_frequently_nhds {X : Type u} {x : X} [] {p : XProp} :
(∃ᶠ (x' : X) in nhds x, ∃ᶠ (x'' : X) in nhds x', p x'') ∃ᶠ (x : X) in nhds x, p x
@[simp]
theorem eventually_mem_nhds {X : Type u} {x : X} {s : Set X} [] :
(∀ᶠ (x' : X) in nhds x, s nhds x') s nhds x
@[simp]
theorem nhds_bind_nhds {X : Type u} {x : X} [] :
(nhds x).bind nhds = nhds x
@[simp]
theorem eventually_eventuallyEq_nhds {X : Type u} {α : Type u_1} {x : X} [] {f : Xα} {g : Xα} :
(∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g) f =ᶠ[nhds x] g
theorem Filter.EventuallyEq.eq_of_nhds {X : Type u} {α : Type u_1} {x : X} [] {f : Xα} {g : Xα} (h : f =ᶠ[nhds x] g) :
f x = g x
@[simp]
theorem eventually_eventuallyLE_nhds {X : Type u} {α : Type u_1} {x : X} [] [LE α] {f : Xα} {g : Xα} :
(∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g) f ≤ᶠ[nhds x] g
theorem Filter.EventuallyEq.eventuallyEq_nhds {X : Type u} {α : Type u_1} {x : X} [] {f : Xα} {g : Xα} (h : f =ᶠ[nhds x] g) :
∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g

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

theorem Filter.EventuallyLE.eventuallyLE_nhds {X : Type u} {α : Type u_1} {x : X} [] [LE α] {f : Xα} {g : Xα} (h : f ≤ᶠ[nhds x] g) :
∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g

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

theorem all_mem_nhds {X : Type u} [] (x : X) (P : Set XProp) (hP : ∀ (s t : Set X), s tP sP t) :
(snhds x, P s) ∀ (s : Set X), x sP s
theorem all_mem_nhds_filter {X : Type u} {α : Type u_1} [] (x : X) (f : Set XSet α) (hf : ∀ (s t : Set X), s tf s f t) (l : ) :
(snhds x, f s l) ∀ (s : Set X), x sf s l
theorem tendsto_nhds {X : Type u} {α : Type u_1} {x : X} [] {f : αX} {l : } :
Filter.Tendsto f l (nhds x) ∀ (s : Set X), x sf ⁻¹' s l
theorem tendsto_atTop_nhds {X : Type u} {α : Type u_1} {x : X} [] [] [] {f : αX} :
Filter.Tendsto f Filter.atTop (nhds x) ∀ (U : Set X), x U∃ (N : α), ∀ (n : α), N nf n U
theorem tendsto_const_nhds {X : Type u} {α : Type u_1} {x : X} [] {f : } :
Filter.Tendsto (fun (x_1 : α) => x) f (nhds x)
theorem tendsto_atTop_of_eventually_const {X : Type u} {x : X} [] {ι : Type u_3} [] [] {u : ιX} {i₀ : ι} (h : ii₀, u i = x) :
Filter.Tendsto u Filter.atTop (nhds x)
theorem tendsto_atBot_of_eventually_const {X : Type u} {x : X} [] {ι : Type u_3} [] [] {u : ιX} {i₀ : ι} (h : ii₀, u i = x) :
Filter.Tendsto u Filter.atBot (nhds x)
theorem pure_le_nhds {X : Type u} [] :
pure nhds
theorem tendsto_pure_nhds {X : Type u} {α : Type u_1} [] (f : αX) (a : α) :
Filter.Tendsto f (pure a) (nhds (f a))
theorem OrderTop.tendsto_atTop_nhds {X : Type u} {α : Type u_1} [] [] [] (f : αX) :
Filter.Tendsto f Filter.atTop (nhds (f ))
@[simp]
instance nhds_neBot {X : Type u} {x : X} [] :
(nhds x).NeBot
Equations
• =
theorem tendsto_nhds_of_eventually_eq {X : Type u} {α : Type u_1} {x : X} [] {l : } {f : αX} (h : ∀ᶠ (x' : α) in l, f x' = x) :
theorem Filter.EventuallyEq.tendsto {X : Type u} {α : Type u_1} {x : X} [] {l : } {f : αX} (hf : f =ᶠ[l] fun (x_1 : α) => x) :

### Cluster points #

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

theorem ClusterPt.neBot {X : Type u} {x : X} [] {F : } (h : ) :
(nhds x F).NeBot
theorem Filter.HasBasis.clusterPt_iff {X : Type u} {x : X} [] {ιX : Sort u_3} {ιF : Sort u_4} {pX : ιXProp} {sX : ιXSet X} {pF : ιFProp} {sF : ιFSet X} {F : } (hX : (nhds x).HasBasis pX sX) (hF : F.HasBasis pF sF) :
∀ ⦃i : ιX⦄, pX i∀ ⦃j : ιF⦄, pF j(sX i sF j).Nonempty
theorem clusterPt_iff {X : Type u} {x : X} [] {F : } :
∀ ⦃U : Set X⦄, U nhds x∀ ⦃V : Set X⦄, V F(U V).Nonempty
theorem clusterPt_iff_not_disjoint {X : Type u} {x : X} [] {F : } :
theorem clusterPt_principal_iff {X : Type u} {x : X} {s : Set X} [] :
Unhds x, (U s).Nonempty

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

theorem clusterPt_principal_iff_frequently {X : Type u} {x : X} {s : Set X} [] :
∃ᶠ (y : X) in nhds x, y s
theorem ClusterPt.of_le_nhds {X : Type u} {x : X} [] {f : } (H : f nhds x) [f.NeBot] :
theorem ClusterPt.of_le_nhds' {X : Type u} {x : X} [] {f : } (H : f nhds x) (_hf : f.NeBot) :
theorem ClusterPt.of_nhds_le {X : Type u} {x : X} [] {f : } (H : nhds x f) :
theorem ClusterPt.mono {X : Type u} {x : X} [] {f : } {g : } (H : ) (h : f g) :
theorem ClusterPt.of_inf_left {X : Type u} {x : X} [] {f : } {g : } (H : ClusterPt x (f g)) :
theorem ClusterPt.of_inf_right {X : Type u} {x : X} [] {f : } {g : } (H : ClusterPt x (f g)) :
theorem Ultrafilter.clusterPt_iff {X : Type u} {x : X} [] {f : } :
ClusterPt x f f nhds x
theorem clusterPt_iff_ultrafilter {X : Type u} {x : X} [] {f : } :
∃ (u : ), u f u nhds x
theorem mapClusterPt_def {X : Type u} [] {ι : Type u_3} (x : X) (F : ) (u : ιX) :
theorem mapClusterPt_iff {X : Type u} [] {ι : Type u_3} (x : X) (F : ) (u : ιX) :
MapClusterPt x F u snhds x, ∃ᶠ (a : ι) in F, u a s
theorem mapClusterPt_iff_ultrafilter {X : Type u} [] {ι : Type u_3} (x : X) (F : ) (u : ιX) :
MapClusterPt x F u ∃ (U : ), U F Filter.Tendsto u (U) (nhds x)
theorem mapClusterPt_comp {X : Type u_3} {α : Type u_4} {β : Type u_5} {x : X} [] {F : } {φ : αβ} {u : βX} :
MapClusterPt x F (u φ) MapClusterPt x () u
theorem mapClusterPt_of_comp {X : Type u} {α : Type u_1} {β : Type u_2} {x : X} [] {F : } {φ : βα} {p : } {u : αX} [p.NeBot] (h : ) (H : Filter.Tendsto (u φ) p (nhds x)) :
theorem acc_iff_cluster {X : Type u} [] (x : X) (F : ) :
AccPt x F ClusterPt x ( F)
theorem acc_principal_iff_cluster {X : Type u} [] (x : X) (C : Set X) :

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

theorem accPt_iff_nhds {X : Type u} [] (x : X) (C : Set X) :
Unhds x, yU 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 {X : Type u} [] (x : X) (C : Set X) :
∃ᶠ (y : X) in nhds x, y x y C

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

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

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

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

theorem interior_eq_nhds' {X : Type u} {s : Set X} [] :
= {x : X | s nhds x}
theorem interior_eq_nhds {X : Type u} {s : Set X} [] :
= {x : X | }
@[simp]
theorem interior_mem_nhds {X : Type u} {x : X} {s : Set X} [] :
theorem interior_setOf_eq {X : Type u} [] {p : XProp} :
interior {x : X | p x} = {x : X | ∀ᶠ (y : X) in nhds x, p y}
theorem isOpen_setOf_eventually_nhds {X : Type u} [] {p : XProp} :
IsOpen {x : X | ∀ᶠ (y : X) in nhds x, p y}
theorem subset_interior_iff_nhds {X : Type u} {s : Set X} [] {V : Set X} :
s xs, V nhds x
theorem isOpen_iff_nhds {X : Type u} {s : Set X} [] :
xs,
theorem TopologicalSpace.ext_iff_nhds {X : Type u} {t : } {t' : } :
t = t' ∀ (x : X), nhds x = nhds x
theorem TopologicalSpace.ext_nhds {X : Type u} {t : } {t' : } :
(∀ (x : X), nhds x = nhds x)t = t'

Alias of the reverse direction of TopologicalSpace.ext_iff_nhds.

theorem isOpen_iff_mem_nhds {X : Type u} {s : Set X} [] :
xs, s nhds x
theorem isOpen_iff_eventually {X : Type u} {s : Set X} [] :
xs, ∀ᶠ (y : X) in nhds x, y s

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

theorem isOpen_iff_ultrafilter {X : Type u} {s : Set X} [] :
xs, ∀ (l : ), l nhds xs l
theorem isOpen_singleton_iff_nhds_eq_pure {X : Type u} [] (x : X) :
IsOpen {x} nhds x = pure x
theorem mem_closure_iff_frequently {X : Type u} {x : X} {s : Set X} [] :
x ∃ᶠ (x : X) in nhds x, x s
theorem Filter.Frequently.mem_closure {X : Type u} {x : X} {s : Set X} [] :
(∃ᶠ (x : X) in nhds x, x s)x

Alias of the reverse direction of mem_closure_iff_frequently.

theorem isClosed_iff_frequently {X : Type u} {s : Set X} [] :
∀ (x : X), (∃ᶠ (y : X) in nhds x, y s)x s

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

theorem isClosed_setOf_clusterPt {X : Type u} [] {f : } :
IsClosed {x : 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 {X : Type u} {x : X} {s : Set X} [] :
x
theorem mem_closure_iff_nhds_ne_bot {X : Type u} {x : X} {s : Set X} [] :
@[deprecated mem_closure_iff_nhds_ne_bot]
theorem mem_closure_iff_nhds_neBot {X : Type u} {x : X} {s : Set X} [] :

Alias of mem_closure_iff_nhds_ne_bot.

theorem mem_closure_iff_nhdsWithin_neBot {X : Type u} {x : X} {s : Set X} [] :
x ().NeBot
theorem nhdsWithin_neBot {X : Type u} {x : X} {s : Set X} [] :
().NeBot ∀ ⦃t : Set X⦄, t nhds x(t s).Nonempty
theorem nhdsWithin_mono {X : Type u} [] (x : X) {s : Set X} {t : Set X} (h : s t) :
theorem not_mem_closure_iff_nhdsWithin_eq_bot {X : Type u} {x : X} {s : Set X} [] :
x =
theorem dense_compl_singleton {X : Type u} [] (x : X) [(nhdsWithin x {x}).NeBot] :

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

theorem closure_compl_singleton {X : Type u} [] (x : X) [(nhdsWithin x {x}).NeBot] :
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 {X : Type u} [] (x : X) [(nhdsWithin x {x}).NeBot] :

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

theorem not_isOpen_singleton {X : Type u} [] (x : X) [(nhdsWithin x {x}).NeBot] :
theorem closure_eq_cluster_pts {X : Type u} {s : Set X} [] :
= {a : X | }
theorem mem_closure_iff_nhds {X : Type u} {x : X} {s : Set X} [] :
x tnhds x, (t s).Nonempty
theorem mem_closure_iff_nhds' {X : Type u} {x : X} {s : Set X} [] :
x tnhds x, ∃ (y : s), y t
theorem mem_closure_iff_comap_neBot {X : Type u} {x : X} {s : Set X} [] :
x (Filter.comap Subtype.val (nhds x)).NeBot
theorem mem_closure_iff_nhds_basis' {X : Type u} {ι : Sort w} {x : X} {t : Set X} [] {p : ιProp} {s : ιSet X} (h : (nhds x).HasBasis p s) :
x ∀ (i : ι), p i(s i t).Nonempty
theorem mem_closure_iff_nhds_basis {X : Type u} {ι : Sort w} {x : X} {t : Set X} [] {p : ιProp} {s : ιSet X} (h : (nhds x).HasBasis p s) :
x ∀ (i : ι), p iyt, y s i
theorem clusterPt_iff_forall_mem_closure {X : Type u} {x : X} [] {F : } :
sF, x
theorem clusterPt_iff_lift'_closure {X : Type u} {x : X} [] {F : } :
pure x F.lift' closure
theorem clusterPt_iff_lift'_closure' {X : Type u} {x : X} [] {F : } :
(F.lift' closure pure x).NeBot
@[simp]
theorem clusterPt_lift'_closure_iff {X : Type u} {x : X} [] {F : } :
ClusterPt x (F.lift' closure)
theorem mem_closure_iff_ultrafilter {X : Type u} {x : X} {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 {X : Type u} {s : Set X} [] :
∀ (a : X), a s
theorem isClosed_iff_ultrafilter {X : Type u} {s : Set X} [] :
∀ (x : X) (u : ), u nhds xs ux s
theorem isClosed_iff_nhds {X : Type u} {s : Set X} [] :
∀ (x : X), (Unhds x, (U s).Nonempty)x s
theorem isClosed_iff_forall_filter {X : Type u} {s : Set X} [] :
∀ (x : X) (F : ), F.NeBotF nhds xx s
theorem IsClosed.interior_union_left {X : Type u} {s : Set X} {t : Set X} [] :
interior (s t) s
theorem IsClosed.interior_union_right {X : Type u} {s : Set X} {t : Set X} [] (h : ) :
theorem IsOpen.inter_closure {X : Type u} {s : Set X} {t : Set X} [] (h : ) :
s closure (s t)
theorem IsOpen.closure_inter {X : Type u} {s : Set X} {t : Set X} [] (h : ) :
t closure (s t)
theorem Dense.open_subset_closure_inter {X : Type u} {s : Set X} {t : Set X} [] (hs : ) (ht : ) :
t closure (t s)
theorem mem_closure_of_mem_closure_union {X : Type u} {x : X} {s₁ : Set X} {s₂ : Set X} [] (h : x closure (s₁ s₂)) (h₁ : s₁ nhds x) :
x closure s₂
theorem Dense.inter_of_isOpen_left {X : Type u} {s : Set X} {t : Set X} [] (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_isOpen_right {X : Type u} {s : Set X} {t : Set X} [] (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 {X : Type u} {x : X} {s : Set X} {t : Set X} [] (hs : ) (ht : t nhds x) :
(s t).Nonempty
theorem closure_diff {X : Type u} {s : Set X} {t : Set X} [] :
\ closure (s \ t)
theorem Filter.Frequently.mem_of_closed {X : Type u} {x : X} {s : Set X} [] (h : ∃ᶠ (x : X) in nhds x, x s) (hs : ) :
x s
theorem IsClosed.mem_of_frequently_of_tendsto {X : Type u} {α : Type u_1} {x : X} {s : Set X} [] {f : αX} {b : } (hs : ) (h : ∃ᶠ (x : α) in b, f x s) (hf : Filter.Tendsto f b (nhds x)) :
x s
theorem IsClosed.mem_of_tendsto {X : Type u} {α : Type u_1} {x : X} {s : Set X} [] {f : αX} {b : } [b.NeBot] (hs : ) (hf : Filter.Tendsto f b (nhds x)) (h : ∀ᶠ (x : α) in b, f x s) :
x s
theorem mem_closure_of_frequently_of_tendsto {X : Type u} {α : Type u_1} {x : X} {s : Set X} [] {f : αX} {b : } (h : ∃ᶠ (x : α) in b, f x s) (hf : Filter.Tendsto f b (nhds x)) :
x
theorem mem_closure_of_tendsto {X : Type u} {α : Type u_1} {x : X} {s : Set X} [] {f : αX} {b : } [b.NeBot] (hf : Filter.Tendsto f b (nhds x)) (h : ∀ᶠ (x : α) in b, f x s) :
x
theorem tendsto_inf_principal_nhds_iff_of_forall_eq {X : Type u} {α : Type u_1} {x : X} [] {f : αX} {l : } {s : Set α} (h : as, f a = x) :

Suppose that f sends the complement to s to a single point x, and l is some filter. Then f tends to x along l restricted to s if and only if it tends to x 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. These 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 = x is not equivalent to Filter.Tendsto g f (𝓝 x) unless the codomain is a Hausdorff space and g has a limit along f.

theorem le_nhds_lim {X : Type u} [] {f : } (h : ∃ (x : X), f nhds x) :
f nhds (lim f)

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

theorem tendsto_nhds_limUnder {X : Type u} {α : Type u_1} [] {f : } {g : αX} (h : ∃ (x : X), Filter.Tendsto g f (nhds x)) :

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

### Continuity #

theorem continuous_def {X : Type u_1} {Y : Type u_2} :
∀ {x : } {x_1 : } {f : XY}, ∀ (s : Set Y), IsOpen (f ⁻¹' s)
theorem IsOpen.preimage {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) {t : Set Y} (h : ) :
theorem continuous_congr {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {g : XY} (h : ∀ (x : X), f x = g x) :
theorem Continuous.congr {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {g : XY} (h : ) (h' : ∀ (x : X), f x = g x) :
theorem ContinuousAt.tendsto {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} (h : ) :
Filter.Tendsto f (nhds x) (nhds (f x))
theorem continuousAt_def {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} :
Anhds (f x), f ⁻¹' A nhds x
theorem continuousAt_congr {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} {g : XY} (h : f =ᶠ[nhds x] g) :
theorem ContinuousAt.congr {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} {g : XY} (hf : ) (h : f =ᶠ[nhds x] g) :
theorem ContinuousAt.preimage_mem_nhds {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} {t : Set Y} (h : ) (ht : t nhds (f x)) :
theorem ContinuousAt.eventually_mem {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} (hf : ) {s : Set Y} (hs : s nhds (f x)) :
∀ᶠ (y : X) in nhds x, f y s

If f x ∈ s ∈ 𝓝 (f x) for continuous f, then f y ∈ s near x.

This is essentially Filter.Tendsto.eventually_mem, but infers in more cases when applied.

@[deprecated]
theorem eventuallyEq_zero_nhds {X : Type u_1} [] {x : X} {M₀ : Type u_4} [Zero M₀] {f : XM₀} :
f =ᶠ[nhds x] 0 x

Deprecated, please use not_mem_tsupport_iff_eventuallyEq instead.

theorem ClusterPt.map {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} {lx : } {ly : } (H : ClusterPt x lx) (hfc : ) (hf : Filter.Tendsto f lx ly) :
ClusterPt (f x) ly
theorem preimage_interior_subset_interior_preimage {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {t : Set Y} (hf : ) :

See also interior_preimage_subset_preimage_interior.

theorem continuous_id {X : Type u_1} [] :
theorem continuous_id' {X : Type u_1} [] :
Continuous fun (x : X) => x
theorem Continuous.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XY} {g : YZ} (hg : ) (hf : ) :
theorem Continuous.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XY} {g : YZ} (hg : ) (hf : ) :
Continuous fun (x : X) => g (f x)
theorem Continuous.iterate {X : Type u_1} [] {f : XX} (h : ) (n : ) :
theorem ContinuousAt.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XY} {x : X} {g : YZ} (hg : ContinuousAt g (f x)) (hf : ) :
theorem ContinuousAt.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XY} {g : YZ} {x : X} (hg : ContinuousAt g (f x)) (hf : ) :
ContinuousAt (fun (x : X) => g (f x)) x
theorem ContinuousAt.comp_of_eq {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [] [] [] {f : XY} {x : X} {y : Y} {g : YZ} (hg : ) (hf : ) (hy : f x = y) :

See note [comp_of_eq lemmas]

theorem Continuous.tendsto {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (x : X) :
Filter.Tendsto f (nhds x) (nhds (f x))
theorem Continuous.tendsto' {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (x : X) (y : 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 {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} (h : ) :
theorem continuous_iff_continuousAt {X : Type u_1} {Y : Type u_2} [] [] {f : XY} :
∀ (x : X),
theorem continuousAt_const {X : Type u_1} {Y : Type u_2} [] [] {x : X} {y : Y} :
ContinuousAt (fun (x : X) => y) x
theorem continuous_const {X : Type u_1} {Y : Type u_2} [] [] {y : Y} :
Continuous fun (x : X) => y
theorem Filter.EventuallyEq.continuousAt {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} {y : Y} (h : f =ᶠ[nhds x] fun (x : X) => y) :
theorem continuous_of_const {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (h : ∀ (x y : X), f x = f y) :
theorem continuousAt_id {X : Type u_1} [] {x : X} :
theorem continuousAt_id' {X : Type u_1} [] (y : X) :
ContinuousAt (fun (x : X) => x) y
theorem ContinuousAt.iterate {X : Type u_1} [] {x : X} {f : XX} (hf : ) (hx : f x = x) (n : ) :
theorem continuous_iff_isClosed {X : Type u_1} {Y : Type u_2} [] [] {f : XY} :
∀ (s : Set Y), IsClosed (f ⁻¹' s)
theorem IsClosed.preimage {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) {t : Set Y} (h : ) :
theorem mem_closure_image {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} {x : X} (hf : ) (hx : x ) :
f x closure (f '' s)
theorem continuousAt_iff_ultrafilter {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {x : X} :
∀ (g : ), g nhds xFilter.Tendsto f (g) (nhds (f x))
theorem continuous_iff_ultrafilter {X : Type u_1} {Y : Type u_2} [] [] {f : XY} :
∀ (x : X) (g : ), g nhds xFilter.Tendsto f (g) (nhds (f x))
theorem Continuous.closure_preimage_subset {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (t : Set Y) :
theorem Continuous.frontier_preimage_subset {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (t : Set Y) :
theorem Set.MapsTo.closure {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} {t : Set Y} (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 {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (h : ) :
f '' closure (f '' s)

See also IsClosedMap.closure_image_eq_of_continuous.

theorem closure_image_closure {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (h : ) :
closure (f '' ) = closure (f '' s)
theorem closure_subset_preimage_closure_image {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} (h : ) :
f ⁻¹' closure (f '' s)
theorem map_mem_closure {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} {x : X} {t : Set Y} (hf : ) (hx : x ) (ht : Set.MapsTo f s t) :
f x
theorem Set.MapsTo.closure_left {X : Type u_1} {Y : Type u_2} [] [] {f : XY} {s : Set X} {t : Set Y} (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.

theorem Filter.Tendsto.lift'_closure {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) {l : } {l' : } (h : Filter.Tendsto f l l') :
Filter.Tendsto f (l.lift' closure) (l'.lift' closure)
theorem tendsto_lift'_closure_nhds {X : Type u_1} {Y : Type u_2} [] [] {f : XY} (hf : ) (x : X) :
Filter.Tendsto f ((nhds x).lift' closure) ((nhds (f x)).lift' closure)

### Function with dense range #

theorem Function.Surjective.denseRange {X : Type u_1} [] {α : Type u_4} {f : αX} (hf : ) :

A surjective map has dense range.

theorem denseRange_id {X : Type u_1} [] :
theorem denseRange_iff_closure_range {X : Type u_1} [] {α : Type u_4} {f : αX} :
closure () = Set.univ
theorem DenseRange.closure_range {X : Type u_1} [] {α : Type u_4} {f : αX} (h : ) :
closure () = Set.univ
theorem Dense.denseRange_val {X : Type u_1} [] {s : Set X} (h : ) :
DenseRange Subtype.val
theorem Continuous.range_subset_closure_image_dense {X : Type u_1} {Y : Type u_2} [] [] {s : Set X} {f : XY} (hf : ) (hs : ) :
closure (f '' s)
theorem DenseRange.dense_image {X : Type u_1} {Y : Type u_2} [] [] {s : Set X} {f : XY} (hf' : ) (hf : ) (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 {X : Type u_1} [] {α : Type u_4} {f : αX} {s : Set X} (hf : ) (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 {X : Type u_1} {Y : Type u_2} [] [] {s : Set X} {f : XY} (hf' : ) (hf : ) (hs : ) {t : Set Y} (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 {Y : Type u_2} {Z : Type u_3} [] [] {α : Type u_4} {g : YZ} {f : αY} (hg : ) (hf : ) (cg : ) :

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

theorem DenseRange.nonempty_iff {X : Type u_1} [] {α : Type u_4} {f : αX} (hf : ) :
theorem DenseRange.nonempty {X : Type u_1} [] {α : Type u_4} {f : αX} [h : ] (hf : ) :
def DenseRange.some {X : Type u_1} [] {α : Type u_4} {f : αX} (hf : ) (x : X) :
α

Given a function f : X → Y with dense range and y : Y, returns some x : X.

Equations
• hf.some x =
Instances For
theorem DenseRange.exists_mem_open {X : Type u_1} [] {α : Type u_4} {f : αX} {s : Set X} (hf : ) (ho : ) (hs : s.Nonempty) :
∃ (a : α), f a s
theorem DenseRange.mem_nhds {X : Type u_1} [] {x : X} {α : Type u_4} {f : αX} {s : Set X} (h : ) (hs : s nhds x) :
∃ (a : α), f a s