Documentation

Mathlib.Topology.Basic

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.

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 #

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)} :
    IsOpen s p s
    theorem TopologicalSpace.ext {X : Type u} {f : TopologicalSpace X} {g : TopologicalSpace X} :
    IsOpen = IsOpenf = g
    theorem TopologicalSpace.ext_iff {X : Type u} {t : TopologicalSpace X} {t' : TopologicalSpace X} :
    t = t' ∀ (s : Set X), IsOpen s IsOpen s
    theorem isOpen_iUnion {X : Type u} {ι : Sort w} [TopologicalSpace X] {f : ιSet X} (h : ∀ (i : ι), IsOpen (f i)) :
    IsOpen (⋃ (i : ι), f i)
    theorem isOpen_biUnion {X : Type u} {α : Type u_1} [TopologicalSpace X] {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} [TopologicalSpace X] (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) :
    IsOpen (s₁ s₂)
    theorem isOpen_iff_of_cover {X : Type u} {α : Type u_1} {s : Set X} [TopologicalSpace X] {f : αSet X} (ho : ∀ (i : α), IsOpen (f i)) (hU : ⋃ (i : α), f i = Set.univ) :
    IsOpen s ∀ (i : α), IsOpen (f i s)
    @[simp]
    theorem Set.Finite.isOpen_sInter {X : Type u} [TopologicalSpace X] {s : Set (Set X)} (hs : s.Finite) :
    (ts, IsOpen t)IsOpen (⋂₀ s)
    theorem Set.Finite.isOpen_biInter {X : Type u} {α : Type u_1} [TopologicalSpace X] {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} [TopologicalSpace X] [Finite ι] {s : ιSet X} (h : ∀ (i : ι), IsOpen (s i)) :
    IsOpen (⋂ (i : ι), s i)
    theorem isOpen_biInter_finset {X : Type u} {α : Type u_1} [TopologicalSpace X] {s : Finset α} {f : αSet X} (h : is, IsOpen (f i)) :
    IsOpen (is, f i)
    @[simp]
    theorem isOpen_const {X : Type u} [TopologicalSpace X] {p : Prop} :
    IsOpen {_x : X | p}
    theorem IsOpen.and {X : Type u} {p₁ : XProp} {p₂ : XProp} [TopologicalSpace X] :
    IsOpen {x : X | p₁ x}IsOpen {x : X | p₂ x}IsOpen {x : X | p₁ x p₂ x}
    @[simp]
    theorem TopologicalSpace.ext_iff_isClosed {X : Type u} {t₁ : TopologicalSpace X} {t₂ : TopologicalSpace X} :
    t₁ = t₂ ∀ (s : Set X), IsClosed s IsClosed s
    theorem TopologicalSpace.ext_isClosed {X : Type u} {t₁ : TopologicalSpace X} {t₂ : TopologicalSpace X} :
    (∀ (s : Set X), IsClosed s IsClosed s)t₁ = t₂

    Alias of the reverse direction of TopologicalSpace.ext_iff_isClosed.

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

    Alias of the reverse direction of isClosed_compl_iff.

    theorem IsOpen.sdiff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : IsOpen s) (h₂ : IsClosed t) :
    IsOpen (s \ t)
    theorem IsClosed.inter {X : Type u} {s₁ : Set X} {s₂ : Set X} [TopologicalSpace X] (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) :
    IsClosed (s₁ s₂)
    theorem IsClosed.sdiff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : IsClosed s) (h₂ : IsOpen t) :
    IsClosed (s \ t)
    theorem Set.Finite.isClosed_biUnion {X : Type u} {α : Type u_1} [TopologicalSpace X] {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} [TopologicalSpace X] {s : Finset α} {f : αSet X} (h : is, IsClosed (f i)) :
    IsClosed (is, f i)
    theorem isClosed_iUnion_of_finite {X : Type u} {ι : Sort w} [TopologicalSpace X] [Finite ι] {s : ιSet X} (h : ∀ (i : ι), IsClosed (s i)) :
    IsClosed (⋃ (i : ι), s i)
    theorem isClosed_imp {X : Type u} [TopologicalSpace X] {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} [TopologicalSpace X] :
    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} [TopologicalSpace X] :
    x interior s ts, IsOpen t x t
    @[simp]
    theorem isOpen_interior {X : Type u} {s : Set X} [TopologicalSpace X] :
    theorem interior_subset {X : Type u} {s : Set X} [TopologicalSpace X] :
    theorem interior_maximal {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : t s) (h₂ : IsOpen t) :
    theorem IsOpen.interior_eq {X : Type u} {s : Set X} [TopologicalSpace X] (h : IsOpen s) :
    theorem IsOpen.subset_interior_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : IsOpen s) :
    theorem subset_interior_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] :
    t interior s ∃ (U : Set X), IsOpen U t U U s
    theorem interior_subset_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] :
    interior s t ∀ (U : Set X), IsOpen UU sU t
    theorem interior_mono {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : s t) :
    @[simp]
    theorem interior_univ {X : Type u} [TopologicalSpace X] :
    interior Set.univ = Set.univ
    @[simp]
    theorem interior_eq_univ {X : Type u} {s : Set X} [TopologicalSpace X] :
    interior s = Set.univ s = Set.univ
    @[simp]
    @[simp]
    theorem interior_inter {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] :
    theorem Set.Finite.interior_biInter {X : Type u} [TopologicalSpace X] {ι : 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} [TopologicalSpace X] {S : Set (Set X)} (hS : S.Finite) :
    interior (⋂₀ S) = sS, interior s
    @[simp]
    theorem Finset.interior_iInter {X : Type u} [TopologicalSpace X] {ι : Type u_3} (s : Finset ι) (f : ιSet X) :
    interior (is, f i) = is, interior (f i)
    @[simp]
    theorem interior_iInter_of_finite {X : Type u} {ι : Sort w} [TopologicalSpace X] [Finite ι] (f : ιSet X) :
    interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)
    @[simp]
    theorem interior_iInter₂_lt_nat {X : Type u} [TopologicalSpace X] {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} [TopologicalSpace X] {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} [TopologicalSpace X] (h₁ : IsClosed s) (h₂ : interior t = ) :
    theorem isOpen_iff_forall_mem_open {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsOpen s xs, ts, IsOpen t x t
    theorem interior_iInter_subset {X : Type u} {ι : Sort w} [TopologicalSpace X] (s : ιSet X) :
    interior (⋂ (i : ι), s i) ⋂ (i : ι), interior (s i)
    theorem interior_iInter₂_subset {X : Type u} {ι : Sort w} [TopologicalSpace X] (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} [TopologicalSpace X] (S : Set (Set X)) :
    interior (⋂₀ S) sS, interior s
    theorem Filter.HasBasis.lift'_interior {X : Type u} {ι : Sort w} [TopologicalSpace X] {l : Filter X} {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} [TopologicalSpace X] (l : Filter X) :
    l.lift' interior l
    theorem Filter.HasBasis.lift'_interior_eq_self {X : Type u} {ι : Sort w} [TopologicalSpace X] {l : Filter X} {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} [TopologicalSpace X] :
    theorem subset_closure {X : Type u} {s : Set X} [TopologicalSpace X] :
    theorem not_mem_of_not_mem_closure {X : Type u} {s : Set X} [TopologicalSpace X] {P : X} (hP : Pclosure s) :
    Ps
    theorem closure_minimal {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : s t) (h₂ : IsClosed t) :
    theorem Disjoint.closure_left {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (hd : Disjoint s t) (ht : IsOpen t) :
    theorem Disjoint.closure_right {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (hd : Disjoint s t) (hs : IsOpen s) :
    theorem IsClosed.closure_eq {X : Type u} {s : Set X} [TopologicalSpace X] (h : IsClosed s) :
    theorem IsClosed.closure_subset {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) :
    theorem IsClosed.closure_subset_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : IsClosed t) :
    closure s t s t
    theorem IsClosed.mem_iff_closure_subset {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) :
    x s closure {x} s
    theorem closure_mono {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : s t) :
    theorem monotone_closure (X : Type u_3) [TopologicalSpace X] :
    Monotone closure
    theorem diff_subset_closure_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] :
    @[simp]
    theorem closure_empty_iff {X : Type u} [TopologicalSpace X] (s : Set X) :
    @[simp]
    theorem closure_nonempty_iff {X : Type u} {s : Set X} [TopologicalSpace X] :
    (closure s).Nonempty s.Nonempty
    theorem Set.Nonempty.of_closure {X : Type u} {s : Set X} [TopologicalSpace X] :
    (closure s).Nonemptys.Nonempty

    Alias of the forward direction of closure_nonempty_iff.

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

    Alias of the reverse direction of closure_nonempty_iff.

    @[simp]
    theorem closure_univ {X : Type u} [TopologicalSpace X] :
    closure Set.univ = Set.univ
    @[simp]
    theorem closure_closure {X : Type u} {s : Set X} [TopologicalSpace X] :
    @[simp]
    theorem closure_union {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] :
    theorem Set.Finite.closure_biUnion {X : Type u} [TopologicalSpace X] {ι : 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} [TopologicalSpace X] {S : Set (Set X)} (hS : S.Finite) :
    closure (⋃₀ S) = sS, closure s
    @[simp]
    theorem Finset.closure_biUnion {X : Type u} [TopologicalSpace X] {ι : Type u_3} (s : Finset ι) (f : ιSet X) :
    closure (is, f i) = is, closure (f i)
    @[simp]
    theorem closure_iUnion_of_finite {X : Type u} {ι : Sort w} [TopologicalSpace X] [Finite ι] (f : ιSet X) :
    closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)
    @[simp]
    theorem closure_iUnion₂_lt_nat {X : Type u} [TopologicalSpace X] {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} [TopologicalSpace X] {n : } (f : Set X) :
    closure (⋃ (m : ), ⋃ (_ : m n), f m) = ⋃ (m : ), ⋃ (_ : m n), closure (f m)
    @[simp]
    theorem interior_compl {X : Type u} {s : Set X} [TopologicalSpace X] :
    @[simp]
    theorem closure_compl {X : Type u} {s : Set X} [TopologicalSpace X] :
    theorem mem_closure_iff {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x closure s ∀ (o : Set X), IsOpen ox o(o s).Nonempty
    theorem closure_inter_open_nonempty_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsOpen t) :
    (closure s t).Nonempty (s t).Nonempty
    theorem Filter.le_lift'_closure {X : Type u} [TopologicalSpace X] (l : Filter X) :
    l l.lift' closure
    theorem Filter.HasBasis.lift'_closure {X : Type u} {ι : Sort w} [TopologicalSpace X] {l : Filter X} {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} [TopologicalSpace X] {l : Filter X} {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} [TopologicalSpace X] {l : Filter X} :
    l.lift' closure = l =
    theorem dense_iff_closure_eq {X : Type u} {s : Set X} [TopologicalSpace X] :
    Dense s closure s = Set.univ
    theorem Dense.closure_eq {X : Type u} {s : Set X} [TopologicalSpace X] :
    Dense sclosure s = Set.univ

    Alias of the forward direction of dense_iff_closure_eq.

    theorem Dense.interior_compl {X : Type u} {s : Set X} [TopologicalSpace X] (h : Dense s) :
    @[simp]
    theorem dense_closure {X : Type u} {s : Set X} [TopologicalSpace 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} [TopologicalSpace X] :
    Dense sDense (closure s)

    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} [TopologicalSpace X] :
    Dense (closure s)Dense s

    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} [TopologicalSpace X] :
    Dense Set.univ
    theorem dense_iff_inter_open {X : Type u} {s : Set X} [TopologicalSpace X] :
    Dense s ∀ (U : Set X), IsOpen UU.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} [TopologicalSpace X] :
    Dense s∀ (U : Set X), IsOpen UU.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} [TopologicalSpace X] (hs : Dense s) {U : Set X} (ho : IsOpen U) (hne : U.Nonempty) :
    xs, x U
    theorem Dense.nonempty_iff {X : Type u} {s : Set X} [TopologicalSpace X] (hs : Dense s) :
    s.Nonempty Nonempty X
    theorem Dense.nonempty {X : Type u} {s : Set X} [TopologicalSpace X] [h : Nonempty X] (hs : Dense s) :
    s.Nonempty
    theorem Dense.mono {X : Type u} {s₁ : Set X} {s₂ : Set X} [TopologicalSpace X] (h : s₁ s₂) (hd : Dense s₁) :
    Dense s₂

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

    Frontier of a set #

    @[simp]

    Interior and frontier are disjoint.

    @[simp]
    @[simp]
    theorem self_diff_frontier {X : Type u} [TopologicalSpace X] (s : Set X) :
    theorem IsClosed.frontier_subset {X : Type u} {s : Set X} [TopologicalSpace X] :

    Alias of the reverse direction of frontier_subset_iff_isClosed.

    @[simp]
    theorem frontier_compl {X : Type u} [TopologicalSpace X] (s : Set X) :

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

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

    The frontier of a set is closed.

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

    The frontier of a closed set has no interior point.

    theorem Disjoint.frontier_left {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (ht : IsOpen t) (hd : Disjoint s t) :
    theorem Disjoint.frontier_right {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (hs : IsOpen s) (hd : Disjoint s t) :

    Neighborhoods #

    theorem nhds_def' {X : Type u} [TopologicalSpace X] (x : X) :
    nhds x = ⨅ (s : Set X), ⨅ (_ : IsOpen s), ⨅ (_ : x s), Filter.principal s
    theorem nhds_basis_opens {X : Type u} [TopologicalSpace X] (x : X) :
    (nhds x).HasBasis (fun (s : Set X) => x s IsOpen 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} [TopologicalSpace X] (x : X) :
    (nhds x).HasBasis (fun (s : Set X) => xs IsClosed s) compl
    @[simp]
    theorem lift'_nhds_interior {X : Type u} [TopologicalSpace X] (x : X) :
    (nhds x).lift' interior = nhds x
    theorem Filter.HasBasis.nhds_interior {X : Type u} {ι : Sort w} [TopologicalSpace X] {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} [TopologicalSpace X] {f : Filter X} :
    f nhds x ∀ (s : Set X), x sIsOpen 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} [TopologicalSpace X] {f : Filter X} (h : x s) (o : IsOpen s) (sf : Filter.principal s f) :
    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} [TopologicalSpace X] :
    s nhds x ts, IsOpen t x t
    theorem eventually_nhds_iff {X : Type u} {x : X} [TopologicalSpace X] {p : XProp} :
    (∀ᶠ (y : X) in nhds x, p y) ∃ (t : Set X), (yt, p y) IsOpen t 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 frequently_nhds_iff {X : Type u} {x : X} [TopologicalSpace X] {p : XProp} :
    (∃ᶠ (y : X) in nhds x, p y) ∀ (U : Set X), x UIsOpen UyU, p y
    theorem mem_interior_iff_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    theorem map_nhds {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {f : Xα} :
    Filter.map f (nhds x) = s{s : Set X | x s IsOpen s}, Filter.principal (f '' s)
    theorem mem_of_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    s nhds xx s
    theorem Filter.Eventually.self_of_nhds {X : Type u} {x : X} [TopologicalSpace 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} [TopologicalSpace X] (hs : IsOpen s) (hx : x s) :
    s nhds x
    theorem IsOpen.mem_nhds_iff {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsOpen s) :
    s nhds x x s
    theorem IsClosed.compl_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) (hx : xs) :
    theorem IsOpen.eventually_mem {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsOpen s) (hx : x s) :
    ∀ᶠ (x : X) in nhds x, x s
    theorem nhds_basis_opens' {X : Type u} [TopologicalSpace X] (x : X) :
    (nhds x).HasBasis (fun (s : Set X) => s nhds x IsOpen s) 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} [TopologicalSpace X] {U : Set X} (h : xs, U nhds x) :
    ∃ (V : Set X), s V IsOpen 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} [TopologicalSpace X] {U : Set X} (h : U xs, nhds x) :
    ∃ (V : Set X), s V IsOpen 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} [TopologicalSpace 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} [TopologicalSpace 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} [TopologicalSpace 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} [TopologicalSpace X] :
    (∀ᶠ (x' : X) in nhds x, s nhds x') s nhds x
    @[simp]
    theorem nhds_bind_nhds {X : Type u} {x : X} [TopologicalSpace X] :
    (nhds x).bind nhds = nhds x
    @[simp]
    theorem eventually_eventuallyEq_nhds {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace 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} [TopologicalSpace 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} [TopologicalSpace 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} [TopologicalSpace 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} [TopologicalSpace 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} [TopologicalSpace X] (x : X) (P : Set XProp) (hP : ∀ (s t : Set X), s tP sP t) :
    (snhds x, P s) ∀ (s : Set X), IsOpen sx sP s
    theorem all_mem_nhds_filter {X : Type u} {α : Type u_1} [TopologicalSpace X] (x : X) (f : Set XSet α) (hf : ∀ (s t : Set X), s tf s f t) (l : Filter α) :
    (snhds x, f s l) ∀ (s : Set X), IsOpen sx sf s l
    theorem tendsto_nhds {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {f : αX} {l : Filter α} :
    Filter.Tendsto f l (nhds x) ∀ (s : Set X), IsOpen sx sf ⁻¹' s l
    theorem tendsto_atTop_nhds {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] [Nonempty α] [SemilatticeSup α] {f : αX} :
    Filter.Tendsto f Filter.atTop (nhds x) ∀ (U : Set X), x UIsOpen U∃ (N : α), ∀ (n : α), N nf n U
    theorem tendsto_const_nhds {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {f : Filter α} :
    Filter.Tendsto (fun (x_1 : α) => x) f (nhds x)
    theorem tendsto_atTop_of_eventually_const {X : Type u} {x : X} [TopologicalSpace X] {ι : Type u_3} [SemilatticeSup ι] [Nonempty ι] {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} [TopologicalSpace X] {ι : Type u_3} [SemilatticeInf ι] [Nonempty ι] {u : ιX} {i₀ : ι} (h : ii₀, u i = x) :
    Filter.Tendsto u Filter.atBot (nhds x)
    theorem pure_le_nhds {X : Type u} [TopologicalSpace X] :
    pure nhds
    theorem tendsto_pure_nhds {X : Type u} {α : Type u_1} [TopologicalSpace X] (f : αX) (a : α) :
    Filter.Tendsto f (pure a) (nhds (f a))
    theorem OrderTop.tendsto_atTop_nhds {X : Type u} {α : Type u_1} [TopologicalSpace X] [PartialOrder α] [OrderTop α] (f : αX) :
    Filter.Tendsto f Filter.atTop (nhds (f ))
    @[simp]
    instance nhds_neBot {X : Type u} {x : X} [TopologicalSpace X] :
    (nhds x).NeBot
    Equations
    • =
    theorem tendsto_nhds_of_eventually_eq {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {l : Filter α} {f : αX} (h : ∀ᶠ (x' : α) in l, f x' = x) :
    theorem Filter.EventuallyEq.tendsto {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {l : Filter α} {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} [TopologicalSpace X] {F : Filter X} (h : ClusterPt x F) :
    (nhds x F).NeBot
    theorem Filter.HasBasis.clusterPt_iff {X : Type u} {x : X} [TopologicalSpace X] {ιX : Sort u_3} {ιF : Sort u_4} {pX : ιXProp} {sX : ιXSet X} {pF : ιFProp} {sF : ιFSet X} {F : Filter X} (hX : (nhds x).HasBasis pX sX) (hF : F.HasBasis pF sF) :
    ClusterPt x F ∀ ⦃i : ιX⦄, pX i∀ ⦃j : ιF⦄, pF j(sX i sF j).Nonempty
    theorem clusterPt_iff {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :
    ClusterPt x F ∀ ⦃U : Set X⦄, U nhds x∀ ⦃V : Set X⦄, V F(U V).Nonempty
    theorem clusterPt_principal_iff {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    ClusterPt x (Filter.principal s) 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} [TopologicalSpace X] :
    ClusterPt x (Filter.principal s) ∃ᶠ (y : X) in nhds x, y s
    theorem ClusterPt.of_le_nhds {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} (H : f nhds x) [f.NeBot] :
    theorem ClusterPt.of_le_nhds' {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} (H : f nhds x) (_hf : f.NeBot) :
    theorem ClusterPt.of_nhds_le {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} (H : nhds x f) :
    theorem ClusterPt.mono {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} {g : Filter X} (H : ClusterPt x f) (h : f g) :
    theorem ClusterPt.of_inf_left {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} {g : Filter X} (H : ClusterPt x (f g)) :
    theorem ClusterPt.of_inf_right {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} {g : Filter X} (H : ClusterPt x (f g)) :
    theorem Ultrafilter.clusterPt_iff {X : Type u} {x : X} [TopologicalSpace X] {f : Ultrafilter X} :
    ClusterPt x f f nhds x
    theorem clusterPt_iff_ultrafilter {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} :
    ClusterPt x f ∃ (u : Ultrafilter X), u f u nhds x
    theorem mapClusterPt_def {X : Type u} [TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι) (u : ιX) :
    theorem mapClusterPt_iff {X : Type u} [TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι) (u : ιX) :
    MapClusterPt x F u snhds x, ∃ᶠ (a : ι) in F, u a s
    theorem mapClusterPt_iff_ultrafilter {X : Type u} [TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι) (u : ιX) :
    MapClusterPt x F u ∃ (U : Ultrafilter ι), U F Filter.Tendsto u (U) (nhds x)
    theorem mapClusterPt_comp {X : Type u_3} {α : Type u_4} {β : Type u_5} {x : X} [TopologicalSpace X] {F : Filter α} {φ : αβ} {u : βX} :
    theorem mapClusterPt_of_comp {X : Type u} {α : Type u_1} {β : Type u_2} {x : X} [TopologicalSpace X] {F : Filter α} {φ : βα} {p : Filter β} {u : αX} [p.NeBot] (h : Filter.Tendsto φ p F) (H : Filter.Tendsto (u φ) p (nhds x)) :
    theorem accPt_sup {X : Type u} [TopologicalSpace X] (x : X) (F : Filter X) (G : Filter X) :
    AccPt x (F G) AccPt x F AccPt x G
    theorem acc_iff_cluster {X : Type u} [TopologicalSpace X] (x : X) (F : Filter 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} [TopologicalSpace X] (x : X) (C : Set X) :
    AccPt x (Filter.principal C) 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} [TopologicalSpace X] (x : X) (C : Set X) :
    AccPt x (Filter.principal C) ∃ᶠ (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} [TopologicalSpace X] {F : Filter X} {G : Filter X} (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 G.

    theorem AccPt.clusterPt {X : Type u} [TopologicalSpace X] (x : X) (F : Filter X) (h : AccPt x F) :

    Interior, closure and frontier in terms of neighborhoods #

    theorem interior_eq_nhds' {X : Type u} {s : Set X} [TopologicalSpace X] :
    interior s = {x : X | s nhds x}
    theorem interior_eq_nhds {X : Type u} {s : Set X} [TopologicalSpace X] :
    @[simp]
    theorem interior_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    theorem interior_setOf_eq {X : Type u} [TopologicalSpace X] {p : XProp} :
    interior {x : X | p x} = {x : X | ∀ᶠ (y : X) in nhds x, p y}
    theorem isOpen_setOf_eventually_nhds {X : Type u} [TopologicalSpace X] {p : XProp} :
    IsOpen {x : X | ∀ᶠ (y : X) in nhds x, p y}
    theorem subset_interior_iff_nhds {X : Type u} {s : Set X} [TopologicalSpace X] {V : Set X} :
    s interior V xs, V nhds x
    theorem isOpen_iff_nhds {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsOpen s xs, nhds x Filter.principal s
    theorem TopologicalSpace.ext_iff_nhds {X : Type u} {t : TopologicalSpace X} {t' : TopologicalSpace X} :
    t = t' ∀ (x : X), nhds x = nhds x
    theorem TopologicalSpace.ext_nhds {X : Type u} {t : TopologicalSpace X} {t' : TopologicalSpace X} :
    (∀ (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} [TopologicalSpace X] :
    IsOpen s xs, s nhds x
    theorem isOpen_iff_eventually {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsOpen s 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} [TopologicalSpace X] :
    IsOpen s xs, ∀ (l : Ultrafilter X), l nhds xs l
    theorem mem_closure_iff_frequently {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x closure s ∃ᶠ (x : X) in nhds x, x s
    theorem Filter.Frequently.mem_closure {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    (∃ᶠ (x : X) in nhds x, x s)x closure s

    Alias of the reverse direction of mem_closure_iff_frequently.

    theorem isClosed_iff_frequently {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsClosed s ∀ (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} [TopologicalSpace X] {f : Filter X} :
    IsClosed {x : X | ClusterPt x f}

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

    @[deprecated mem_closure_iff_nhds_ne_bot]

    Alias of mem_closure_iff_nhds_ne_bot.

    theorem mem_closure_iff_nhdsWithin_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x closure s (nhdsWithin x s).NeBot
    theorem nhdsWithin_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    (nhdsWithin x s).NeBot ∀ ⦃t : Set X⦄, t nhds x(t s).Nonempty
    theorem nhdsWithin_mono {X : Type u} [TopologicalSpace X] (x : X) {s : Set X} {t : Set X} (h : s t) :
    theorem dense_compl_singleton {X : Type u} [TopologicalSpace X] (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} [TopologicalSpace X] (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} [TopologicalSpace X] (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} [TopologicalSpace X] (x : X) [(nhdsWithin x {x}).NeBot] :
    theorem mem_closure_iff_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x closure s tnhds x, (t s).Nonempty
    theorem mem_closure_iff_nhds' {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x closure s tnhds x, ∃ (y : s), y t
    theorem mem_closure_iff_comap_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x closure s (Filter.comap Subtype.val (nhds x)).NeBot
    theorem mem_closure_iff_nhds_basis' {X : Type u} {ι : Sort w} {x : X} {t : Set X} [TopologicalSpace X] {p : ιProp} {s : ιSet X} (h : (nhds x).HasBasis p s) :
    x closure t ∀ (i : ι), p i(s i t).Nonempty
    theorem mem_closure_iff_nhds_basis {X : Type u} {ι : Sort w} {x : X} {t : Set X} [TopologicalSpace X] {p : ιProp} {s : ιSet X} (h : (nhds x).HasBasis p s) :
    x closure t ∀ (i : ι), p iyt, y s i
    theorem clusterPt_iff_forall_mem_closure {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :
    ClusterPt x F sF, x closure s
    theorem clusterPt_iff_lift'_closure {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :
    ClusterPt x F pure x F.lift' closure
    theorem clusterPt_iff_lift'_closure' {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :
    ClusterPt x F (F.lift' closure pure x).NeBot
    @[simp]
    theorem clusterPt_lift'_closure_iff {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :
    ClusterPt x (F.lift' closure) ClusterPt x F
    theorem mem_closure_iff_ultrafilter {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x closure s ∃ (u : Ultrafilter X), 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} [TopologicalSpace X] :
    IsClosed s ∀ (a : X), ClusterPt a (Filter.principal s)a s
    theorem isClosed_iff_ultrafilter {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsClosed s ∀ (x : X) (u : Ultrafilter X), u nhds xs ux s
    theorem isClosed_iff_nhds {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsClosed s ∀ (x : X), (Unhds x, (U s).Nonempty)x s
    theorem isClosed_iff_forall_filter {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsClosed s ∀ (x : X) (F : Filter X), F.NeBotF Filter.principal sF nhds xx s
    theorem IsClosed.interior_union_left {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] :
    theorem IsClosed.interior_union_right {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsClosed t) :
    theorem IsOpen.inter_closure {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsOpen s) :
    theorem IsOpen.closure_inter {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsOpen t) :
    theorem Dense.open_subset_closure_inter {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (hs : Dense s) (ht : IsOpen t) :
    t closure (t s)
    theorem mem_closure_of_mem_closure_union {X : Type u} {x : X} {s₁ : Set X} {s₂ : Set X} [TopologicalSpace 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} [TopologicalSpace X] (hs : Dense s) (ht : Dense t) (hso : IsOpen s) :
    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} [TopologicalSpace X] (hs : Dense s) (ht : Dense t) (hto : IsOpen t) :
    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} [TopologicalSpace X] (hs : Dense s) (ht : t nhds x) :
    (s t).Nonempty
    theorem closure_diff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] :
    theorem Filter.Frequently.mem_of_closed {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (h : ∃ᶠ (x : X) in nhds x, x s) (hs : IsClosed s) :
    x s
    theorem IsClosed.mem_of_frequently_of_tendsto {X : Type u} {α : Type u_1} {x : X} {s : Set X} [TopologicalSpace X] {f : αX} {b : Filter α} (hs : IsClosed s) (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} [TopologicalSpace X] {f : αX} {b : Filter α} [b.NeBot] (hs : IsClosed s) (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} [TopologicalSpace X] {f : αX} {b : Filter α} (h : ∃ᶠ (x : α) in b, f x s) (hf : Filter.Tendsto f b (nhds x)) :
    theorem mem_closure_of_tendsto {X : Type u} {α : Type u_1} {x : X} {s : Set X} [TopologicalSpace X] {f : αX} {b : Filter α} [b.NeBot] (hf : Filter.Tendsto f b (nhds x)) (h : ∀ᶠ (x : α) in b, f x s) :
    theorem tendsto_inf_principal_nhds_iff_of_forall_eq {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {f : αX} {l : Filter α} {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} [TopologicalSpace X] {f : Filter X} (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} [TopologicalSpace X] {f : Filter α} {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 : TopologicalSpace X} {x_1 : TopologicalSpace Y} {f : XY}, Continuous f ∀ (s : Set Y), IsOpen sIsOpen (f ⁻¹' s)
    theorem IsOpen.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Continuous f) {t : Set Y} (h : IsOpen t) :
    theorem continuous_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {g : XY} (h : ∀ (x : X), f x = g x) :
    theorem Continuous.congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {g : XY} (h : Continuous f) (h' : ∀ (x : X), f x = g x) :
    theorem ContinuousAt.tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {x : X} (h : ContinuousAt f x) :
    Filter.Tendsto f (nhds x) (nhds (f x))
    theorem continuousAt_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {x : X} :
    ContinuousAt f x Anhds (f x), f ⁻¹' A nhds x
    theorem continuousAt_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {x : X} {g : XY} (h : f =ᶠ[nhds x] g) :
    theorem ContinuousAt.congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {x : X} {g : XY} (hf : ContinuousAt f x) (h : f =ᶠ[nhds x] g) :
    theorem ContinuousAt.preimage_mem_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {x : X} {t : Set Y} (h : ContinuousAt f x) (ht : t nhds (f x)) :
    theorem ContinuousAt.eventually_mem {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {x : X} (hf : ContinuousAt f x) {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} [TopologicalSpace X] {x : X} {M₀ : Type u_4} [Zero M₀] {f : XM₀} :

    Deprecated, please use not_mem_tsupport_iff_eventuallyEq instead.

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

    See also interior_preimage_subset_preimage_interior.

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

    See note [comp_of_eq lemmas]

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

    See also IsClosedMap.closure_image_eq_of_continuous.

    theorem closure_image_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} (h : Continuous f) :
    theorem closure_subset_preimage_closure_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} (h : Continuous f) :
    theorem map_mem_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} {x : X} {t : Set Y} (hf : Continuous f) (hx : x closure s) (ht : Set.MapsTo f s t) :
    f x closure t
    theorem Set.MapsTo.closure_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} {s : Set X} {t : Set Y} (h : Set.MapsTo f s t) (hc : Continuous f) (ht : IsClosed 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} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Continuous f) {l : Filter X} {l' : Filter Y} (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} [TopologicalSpace X] [TopologicalSpace Y] {f : XY} (hf : Continuous f) (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} [TopologicalSpace X] {α : Type u_4} {f : αX} (hf : Function.Surjective f) :

    A surjective map has dense range.

    theorem denseRange_iff_closure_range {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : αX} :
    theorem DenseRange.closure_range {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : αX} (h : DenseRange f) :
    closure (Set.range f) = Set.univ
    @[simp]
    theorem denseRange_subtype_val {X : Type u_1} [TopologicalSpace X] {p : XProp} :
    DenseRange Subtype.val Dense {x : X | p x}
    theorem Dense.denseRange_val {X : Type u_1} [TopologicalSpace X] {s : Set X} (h : Dense s) :
    DenseRange Subtype.val
    theorem Continuous.range_subset_closure_image_dense {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} (hf : Continuous f) (hs : Dense s) :
    theorem DenseRange.dense_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) :
    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} [TopologicalSpace X] {α : Type u_4} {f : αX} {s : Set X} (hf : DenseRange f) (hs : IsOpen s) :
    s closure (f '' (f ⁻¹' s))

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

    theorem DenseRange.dense_of_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : XY} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) {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} [TopologicalSpace Y] [TopologicalSpace Z] {α : Type u_4} {g : YZ} {f : αY} (hg : DenseRange g) (hf : DenseRange f) (cg : Continuous g) :

    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} [TopologicalSpace X] {α : Type u_4} {f : αX} (hf : DenseRange f) :
    theorem DenseRange.nonempty {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : αX} [h : Nonempty X] (hf : DenseRange f) :
    def DenseRange.some {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : αX} (hf : DenseRange f) (x : X) :
    α

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

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