Documentation

Mathlib.Topology.Basic

Basic theory of topological spaces. #

The main definition is the type class TopologicalSpace α which endows a type α with a topology. Then Set α gets predicates IsOpen, IsClosed and functions interior, closure and frontier. Each point x of α gets a neighborhood filter 𝓝 x. A filter F on α has x as a cluster point if ClusterPt x F : 𝓝 x ⊓ F ≠ ⊥⊓ F ≠ ⊥≠ ⊥⊥. A map f : ι → α→ α clusters at x along F : Filter ι if MapClusterPt x F f : ClusterPt x (map f F). In particular the notion of cluster point of a sequence u is MapClusterPt x atTop u.

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

Notation #

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 #

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

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

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

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

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

A topology on α.

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

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

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

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

    Equations
    • IsOpen = TopologicalSpace.IsOpen

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

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

      isOpen_compl : IsOpen (s)

    A set is closed if its complement is open

    Instances

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

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

      Alias of the reverse direction of isClosed_compl_iff.

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

      Interior of a set #

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

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

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

      Closure of a set #

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

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

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

      Alias of the reverse direction of closure_nonempty_iff.

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

      Alias of the forward direction of closure_nonempty_iff.

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

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

      Equations
      theorem dense_iff_closure_eq {α : Type u} [inst : TopologicalSpace α] {s : Set α} :
      Dense s closure s = Set.univ
      theorem Dense.closure_eq {α : Type u} [inst : TopologicalSpace α] {s : Set α} :
      Dense sclosure s = Set.univ

      Alias of the forward direction of dense_iff_closure_eq.

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

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

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

      Alias of the forward direction of dense_closure.

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

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

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

      Alias of the forward direction of dense_iff_inter_open.

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

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

      Frontier of a set #

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

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

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

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

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

      The frontier of a set is closed.

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

      The frontier of a closed set has no interior point.

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

      Neighborhoods #

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

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

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

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

      Equations

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

      Equations

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

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

      Notation for the filter of punctured neighborhoods of a point.

      Equations

      Notation for the filter of right neighborhoods of a point.

      Equations

      Notation for the filter of left neighborhoods of a point.

      Equations

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

      Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

      theorem exists_open_set_nhds {α : Type u} [inst : TopologicalSpace α] {s : Set α} {U : Set α} (h : ∀ (x : α), x sU nhds x) :
      V, 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' {α : Type u} [inst : TopologicalSpace α] {s : Set α} {U : Set α} (h : U x, h, nhds x) :
      V, 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 {α : Type u} [inst : TopologicalSpace α] {p : αProp} {a : α} (h : Filter.Eventually (fun y => p y) (nhds a)) :
      Filter.Eventually (fun y => Filter.Eventually (fun x => p x) (nhds y)) (nhds a)

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

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

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

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

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

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

      Cluster points #

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

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

      A point x is a cluster point of a filter F if 𝓝 x ⊓ F ≠ ⊥⊓ F ≠ ⊥≠ ⊥⊥. Also known as an accumulation point or a limit point, but beware that terminology varies. This is not the same as asking 𝓝[≠] x ⊓ F ≠ ⊥≠] x ⊓ F ≠ ⊥⊓ F ≠ ⊥≠ ⊥⊥. See mem_closure_iff_clusterPt in particular.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

      Interior, closure and frontier in terms of neighborhoods #

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

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

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

      Alias of the reverse direction of mem_closure_iff_frequently.

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

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

      theorem isClosed_setOf_clusterPt {α : Type u} [inst : TopologicalSpace α] {f : Filter α} :
      IsClosed { 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.

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

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

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

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

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

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

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

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

      theorem isClosed_iff_clusterPt {α : Type u} [inst : TopologicalSpace α] {s : Set α} :
      IsClosed s ∀ (a : α), ClusterPt a (Filter.principal s)a s
      theorem isClosed_iff_nhds {α : Type u} [inst : TopologicalSpace α] {s : Set α} :
      IsClosed s ∀ (x : α), (∀ (U : Set α), U nhds xSet.Nonempty (U s)) → x s
      theorem IsClosed.interior_union_left {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :
      theorem IsClosed.interior_union_right {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (h : IsClosed t) :
      theorem IsOpen.inter_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (h : IsOpen s) :
      theorem IsOpen.closure_inter {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (h : IsOpen t) :
      theorem Dense.open_subset_closure_inter {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (hs : Dense s) (ht : IsOpen t) :
      t closure (t s)
      theorem mem_closure_of_mem_closure_union {α : Type u} [inst : TopologicalSpace α] {s₁ : Set α} {s₂ : Set α} {x : α} (h : x closure (s₁ s₂)) (h₁ : s₁ nhds x) :
      x closure s₂
      theorem Dense.inter_of_open_left {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (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_open_right {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (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 {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} (hs : Dense s) {x : α} (ht : t nhds x) :
      theorem closure_diff {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :
      theorem Filter.Frequently.mem_of_closed {α : Type u} [inst : TopologicalSpace α] {a : α} {s : Set α} (h : Filter.Frequently (fun x => x s) (nhds a)) (hs : IsClosed s) :
      a s
      theorem IsClosed.mem_of_frequently_of_tendsto {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : βα} {b : Filter β} {a : α} {s : Set α} (hs : IsClosed s) (h : Filter.Frequently (fun x => f x s) b) (hf : Filter.Tendsto f b (nhds a)) :
      a s
      theorem IsClosed.mem_of_tendsto {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : βα} {b : Filter β} {a : α} {s : Set α} [inst : Filter.NeBot b] (hs : IsClosed s) (hf : Filter.Tendsto f b (nhds a)) (h : Filter.Eventually (fun x => f x s) b) :
      a s
      theorem mem_closure_of_frequently_of_tendsto {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : βα} {b : Filter β} {a : α} {s : Set α} (h : Filter.Frequently (fun x => f x s) b) (hf : Filter.Tendsto f b (nhds a)) :
      theorem mem_closure_of_tendsto {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : βα} {b : Filter β} {a : α} {s : Set α} [inst : Filter.NeBot b] (hf : Filter.Tendsto f b (nhds a)) (h : Filter.Eventually (fun x => f x s) b) :
      theorem tendsto_inf_principal_nhds_iff_of_forall_eq {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : βα} {l : Filter β} {s : Set β} {a : α} (h : ∀ (x : β), ¬x sf x = a) :

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

      Limits of filters in topological spaces #

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

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

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

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

      If F is an ultrafilter, then Filter.Ultrafilter.lim F is a limit of the filter, if it exists. Note that dot notation F.lim can be used for F : Filter.Ultrafilter α.

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

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

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

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

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

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

      Continuity #

      structure Continuous {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] (f : αβ) :

      A function between topological spaces is continuous if the preimage of every open set is open. Registered as a structure to make sure it is not unfolded by Lean.

      Instances For

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

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

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

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

        See also interior_preimage_subset_preimage_interior.

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

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

        theorem Continuous.continuousAt {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {x : α} (h : Continuous f) :
        theorem continuous_iff_continuousAt {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} :
        Continuous f ∀ (x : α), ContinuousAt f x
        theorem continuousAt_const {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {x : α} {b : β} :
        ContinuousAt (fun x => b) x
        theorem continuous_const {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {b : β} :
        Continuous fun x => b
        theorem Filter.EventuallyEq.continuousAt {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {x : α} {f : αβ} {y : β} (h : f =ᶠ[nhds x] fun x => y) :
        theorem continuous_of_const {α : Type u_2} {β : Type u_1} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (h : ∀ (x y : α), f x = f y) :
        theorem continuousAt_id {α : Type u_1} [inst : TopologicalSpace α] {x : α} :
        theorem ContinuousAt.iterate {α : Type u_1} [inst : TopologicalSpace α] {f : αα} {x : α} (hf : ContinuousAt f x) (hx : f x = x) (n : ) :
        theorem continuous_iff_isClosed {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} :
        Continuous f ∀ (s : Set β), IsClosed sIsClosed (f ⁻¹' s)
        theorem IsClosed.preimage {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Continuous f) {s : Set β} (h : IsClosed s) :
        theorem mem_closure_image {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {x : α} {s : Set α} (hf : ContinuousAt f x) (hx : x closure s) :
        f x closure (f '' s)
        theorem continuousAt_iff_ultrafilter {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {x : α} :
        ContinuousAt f x ∀ (g : Ultrafilter α), g nhds xFilter.Tendsto f (g) (nhds (f x))
        theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} :
        Continuous f ∀ (x : α) (g : Ultrafilter α), g nhds xFilter.Tendsto f (g) (nhds (f x))
        theorem Continuous.closure_preimage_subset {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Continuous f) (t : Set β) :
        theorem Continuous.frontier_preimage_subset {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf : Continuous f) (t : Set β) :
        theorem Set.MapsTo.closure {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {s : Set α} {t : Set β} {f : αβ} (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 {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {s : Set α} (h : Continuous f) :
        f '' closure s closure (f '' s)
        theorem closure_image_closure {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {s : Set α} (h : Continuous f) :
        theorem closure_subset_preimage_closure_image {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} {s : Set α} (h : Continuous f) :
        theorem map_mem_closure {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {s : Set α} {t : Set β} {f : αβ} {a : α} (hf : Continuous f) (ha : a closure s) (ht : Set.MapsTo f s t) :
        f a closure t
        theorem Set.MapsTo.closure_left {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {s : Set α} {t : Set β} {f : αβ} (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.

        Function with dense range #

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

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

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

        A surjective map has dense range.

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

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

        theorem DenseRange.subset_closure_image_preimage_of_isOpen {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κβ} (hf : DenseRange f) {s : Set β} (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 {α : Type u_2} {β : Type u_1} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : αβ} (hf' : DenseRange f) (hf : Continuous f) {s : Set α} (hs : Dense s) {t : Set β} (ht : Set.MapsTo f s t) :

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

        theorem DenseRange.comp {β : Type u_2} {γ : Type u_1} [inst : TopologicalSpace β] [inst : TopologicalSpace γ] {κ : Type u_3} {g : βγ} {f : κβ} (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 {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κβ} (hf : DenseRange f) :
        theorem DenseRange.nonempty {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κβ} [h : Nonempty β] (hf : DenseRange f) :
        def DenseRange.some {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κβ} (hf : DenseRange f) (b : β) :
        κ

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

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