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 .

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 : βˆ€ A βŠ† T, β‹‚β‚€ A ∈ T) (union_mem : βˆ€ A ∈ T, βˆ€ B ∈ T, 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 X β†’ Prop} {h₁ : p Set.univ} {hβ‚‚ : βˆ€ (s t : Set X), p s β†’ p t β†’ p (s ∩ t)} {h₃ : βˆ€ (s : Set (Set X)), (βˆ€ t ∈ s, p t) β†’ p (⋃₀ s)} :
    theorem TopologicalSpace.ext {X : Type u} {f : TopologicalSpace X} {g : TopologicalSpace X} :
    IsOpen = IsOpen β†’ f = 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 : βˆ€ i ∈ s, IsOpen (f i)) :
    IsOpen (⋃ i ∈ s, 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)
    theorem Set.Finite.isOpen_sInter {X : Type u} [TopologicalSpace X] {s : Set (Set X)} (hs : Set.Finite s) :
    (βˆ€ t ∈ s, IsOpen t) β†’ IsOpen (β‹‚β‚€ s)
    theorem Set.Finite.isOpen_biInter {X : Type u} {Ξ± : Type u_1} [TopologicalSpace X] {s : Set Ξ±} {f : Ξ± β†’ Set X} (hs : Set.Finite s) (h : βˆ€ i ∈ s, IsOpen (f i)) :
    IsOpen (β‹‚ i ∈ s, 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 : βˆ€ i ∈ s, IsOpen (f i)) :
    IsOpen (β‹‚ i ∈ s, f i)
    @[simp]
    theorem isOpen_const {X : Type u} [TopologicalSpace X] {p : Prop} :
    IsOpen {_x : X | p}
    theorem IsOpen.and {X : Type u} {p₁ : X β†’ Prop} {pβ‚‚ : X β†’ Prop} [TopologicalSpace X] :
    IsOpen {x : X | p₁ x} β†’ IsOpen {x : X | pβ‚‚ x} β†’ IsOpen {x : X | p₁ x ∧ pβ‚‚ x}
    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)} :
    (βˆ€ t ∈ s, 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 : βˆ€ i ∈ s, IsClosed (f i)) :
    IsClosed (β‹‚ i ∈ s, f i)
    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 : Set.Finite s) (h : βˆ€ i ∈ s, IsClosed (f i)) :
    IsClosed (⋃ i ∈ s, f i)
    theorem isClosed_biUnion_finset {X : Type u} {Ξ± : Type u_1} [TopologicalSpace X] {s : Finset Ξ±} {f : Ξ± β†’ Set X} (h : βˆ€ i ∈ s, IsClosed (f i)) :
    IsClosed (⋃ i ∈ s, 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 : X β†’ Prop} {q : X β†’ Prop} (hp : IsOpen {x : X | p x}) (hq : IsClosed {x : X | q x}) :
    IsClosed {x : X | p x β†’ q x}
    theorem IsClosed.not {X : Type u} {p : X β†’ Prop} [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 ↔ βˆƒ t βŠ† s, IsOpen t ∧ x ∈ t
    @[simp]
    theorem isOpen_interior {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 U β†’ U βŠ† s β†’ U βŠ† 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 : Set.Finite s) (f : ΞΉ β†’ Set X) :
    interior (β‹‚ i ∈ s, f i) = β‹‚ i ∈ s, interior (f i)
    theorem Set.Finite.interior_sInter {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hS : Set.Finite S) :
    interior (β‹‚β‚€ S) = β‹‚ s ∈ S, interior s
    @[simp]
    theorem Finset.interior_iInter {X : Type u} [TopologicalSpace X] {ΞΉ : Type u_3} (s : Finset ΞΉ) (f : ΞΉ β†’ Set X) :
    interior (β‹‚ i ∈ s, f i) = β‹‚ i ∈ s, 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)
    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 ↔ βˆ€ x ∈ s, βˆƒ t βŠ† s, 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 i β†’ Set 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) βŠ† β‹‚ s ∈ S, interior s
    theorem Filter.HasBasis.lift'_interior {X : Type u} {ΞΉ : Sort w} [TopologicalSpace X] {l : Filter X} {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : Filter.HasBasis l p s) :
    Filter.HasBasis (Filter.lift' l interior) p fun (i : ΞΉ) => interior (s i)
    theorem Filter.HasBasis.lift'_interior_eq_self {X : Type u} {ΞΉ : Sort w} [TopologicalSpace X] {l : Filter X} {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : Filter.HasBasis l p s) (ho : βˆ€ (i : ΞΉ), p i β†’ IsOpen (s i)) :
    Filter.lift' l 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 : P βˆ‰ closure s) :
    P βˆ‰ s
    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_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : IsClosed t) :
    theorem IsClosed.mem_iff_closure_subset {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsClosed 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
    @[simp]

    Alias of the forward direction of closure_nonempty_iff.

    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 : Set.Finite s) (f : ΞΉ β†’ Set X) :
    closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)
    theorem Set.Finite.closure_sUnion {X : Type u} [TopologicalSpace X] {S : Set (Set X)} (hS : Set.Finite S) :
    closure (⋃₀ S) = ⋃ s ∈ S, closure s
    @[simp]
    theorem Finset.closure_biUnion {X : Type u} [TopologicalSpace X] {ΞΉ : Type u_3} (s : Finset ΞΉ) (f : ΞΉ β†’ Set X) :
    closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, 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]
    @[simp]
    theorem mem_closure_iff {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x ∈ closure s ↔ βˆ€ (o : Set X), IsOpen o β†’ x ∈ o β†’ Set.Nonempty (o ∩ s)
    theorem Filter.HasBasis.lift'_closure {X : Type u} {ΞΉ : Sort w} [TopologicalSpace X] {l : Filter X} {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (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 {X : Type u} {ΞΉ : Sort w} [TopologicalSpace X] {l : Filter X} {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : Filter.HasBasis l p s) (hc : βˆ€ (i : ΞΉ), p i β†’ IsClosed (s i)) :
    Filter.lift' l 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 s β†’ closure s = Set.univ

    Alias of the forward direction of dense_iff_closure_eq.

    @[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 s β†’ Dense (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 U β†’ Set.Nonempty U β†’ Set.Nonempty (U ∩ s)

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

    theorem Dense.inter_open_nonempty {X : Type u} {s : Set X} [TopologicalSpace X] :
    Dense s β†’ βˆ€ (U : Set X), IsOpen U β†’ Set.Nonempty U β†’ Set.Nonempty (U ∩ s)

    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 : Set.Nonempty U) :
    βˆƒ x ∈ s, x ∈ U
    theorem Dense.nonempty {X : Type u} {s : Set X} [TopologicalSpace X] [h : Nonempty X] (hs : Dense s) :
    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) :
    @[simp]

    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 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) :
    Filter.HasBasis (nhds x) (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) :
    Filter.HasBasis (nhds x) (fun (s : Set X) => x βˆ‰ s ∧ IsClosed s) compl
    @[simp]
    theorem lift'_nhds_interior {X : Type u} [TopologicalSpace X] (x : X) :
    Filter.lift' (nhds x) interior = nhds x
    theorem Filter.HasBasis.nhds_interior {X : Type u} {ΞΉ : Sort w} [TopologicalSpace X] {x : X} {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : Filter.HasBasis (nhds x) p s) :
    Filter.HasBasis (nhds x) 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 ∈ s β†’ IsOpen s β†’ s ∈ 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) :

    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 ↔ βˆƒ t βŠ† s, IsOpen t ∧ x ∈ t
    theorem eventually_nhds_iff {X : Type u} {x : X} [TopologicalSpace X] {p : X β†’ Prop} :
    (βˆ€αΆ  (x : X) in nhds x, p x) ↔ βˆƒ (t : Set X), (βˆ€ x ∈ t, p x) ∧ 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 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 x β†’ x ∈ s
    theorem Filter.Eventually.self_of_nhds {X : Type u} {x : X} [TopologicalSpace X] {p : X β†’ Prop} (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) :
    theorem IsOpen.mem_nhds_iff {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsOpen s) :
    theorem IsClosed.compl_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) (hx : x βˆ‰ s) :
    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) :
    Filter.HasBasis (nhds x) (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 : βˆ€ x ∈ s, 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 ∈ ⨆ x ∈ s, 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 : X β†’ Prop} (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 : X β†’ Prop} :
    (βˆ€αΆ  (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 : X β†’ Prop} :
    (βˆƒαΆ  (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] :
    Filter.bind (nhds x) 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 X β†’ Prop) (hP : βˆ€ (s t : Set X), s βŠ† t β†’ P s β†’ P t) :
    (βˆ€ s ∈ nhds x, P s) ↔ βˆ€ (s : Set X), IsOpen s β†’ x ∈ s β†’ P s
    theorem all_mem_nhds_filter {X : Type u} {Ξ± : Type u_1} [TopologicalSpace X] (x : X) (f : Set X β†’ Set Ξ±) (hf : βˆ€ (s t : Set X), s βŠ† t β†’ f s βŠ† f t) (l : Filter Ξ±) :
    (βˆ€ s ∈ nhds x, f s ∈ l) ↔ βˆ€ (s : Set X), IsOpen s β†’ x ∈ s β†’ f 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 s β†’ x ∈ s β†’ f ⁻¹' 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 ∈ U β†’ IsOpen U β†’ βˆƒ (N : Ξ±), βˆ€ (n : Ξ±), N ≀ n β†’ f 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 : βˆ€ i β‰₯ iβ‚€, 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 : βˆ€ i ≀ iβ‚€, 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] :
    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) :
    theorem Filter.HasBasis.clusterPt_iff {X : Type u} {x : X} [TopologicalSpace X] {ΞΉX : Sort u_3} {ΞΉF : Sort u_4} {pX : ΞΉX β†’ Prop} {sX : ΞΉX β†’ Set X} {pF : ΞΉF β†’ Prop} {sF : ΞΉF β†’ Set X} {F : Filter X} (hX : Filter.HasBasis (nhds x) pX sX) (hF : Filter.HasBasis F pF sF) :
    ClusterPt x F ↔ βˆ€ ⦃i : ΞΉX⦄, pX i β†’ βˆ€ ⦃j : ΞΉF⦄, pF j β†’ Set.Nonempty (sX i ∩ sF j)
    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 β†’ Set.Nonempty (U ∩ V)
    theorem clusterPt_principal_iff {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    ClusterPt x (Filter.principal s) ↔ βˆ€ U ∈ nhds x, Set.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 {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) [Filter.NeBot f] :
    theorem ClusterPt.of_le_nhds' {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} (H : f ≀ nhds x) (_hf : Filter.NeBot f) :
    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 ↔ βˆ€ s ∈ nhds 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_of_comp {X : Type u} {Ξ± : Type u_1} {Ξ² : Type u_2} {x : X} [TopologicalSpace X] {F : Filter Ξ±} {Ο† : Ξ² β†’ Ξ±} {p : Filter Ξ²} {u : Ξ± β†’ X} [Filter.NeBot p] (h : Filter.Tendsto Ο† p F) (H : Filter.Tendsto (u ∘ Ο†) p (nhds 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) ↔ βˆ€ U ∈ nhds x, βˆƒ 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 {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 D.

    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}
    @[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 : X β†’ Prop} :
    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 : X β†’ Prop} :
    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 ↔ βˆ€ x ∈ s, V ∈ nhds x
    theorem isOpen_iff_nhds {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsOpen s ↔ βˆ€ x ∈ s, 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 ↔ βˆ€ x ∈ s, s ∈ nhds x
    theorem isOpen_iff_eventually {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsOpen s ↔ βˆ€ x ∈ s, βˆ€αΆ  (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 ↔ βˆ€ x ∈ s, βˆ€ (l : Ultrafilter X), ↑l ≀ nhds x β†’ s ∈ 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.

    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) [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]

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

    theorem mem_closure_iff_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x ∈ closure s ↔ βˆ€ t ∈ nhds x, Set.Nonempty (t ∩ s)
    theorem mem_closure_iff_nhds' {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :
    x ∈ closure s ↔ βˆ€ t ∈ nhds x, βˆƒ (y : ↑s), ↑y ∈ t
    theorem mem_closure_iff_nhds_basis' {X : Type u} {ΞΉ : Sort w} {x : X} {t : Set X} [TopologicalSpace X] {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : Filter.HasBasis (nhds x) p s) :
    x ∈ closure t ↔ βˆ€ (i : ΞΉ), p i β†’ Set.Nonempty (s i ∩ t)
    theorem mem_closure_iff_nhds_basis {X : Type u} {ΞΉ : Sort w} {x : X} {t : Set X} [TopologicalSpace X] {p : ΞΉ β†’ Prop} {s : ΞΉ β†’ Set X} (h : Filter.HasBasis (nhds x) p s) :
    x ∈ closure t ↔ βˆ€ (i : ΞΉ), p i β†’ βˆƒ y ∈ t, y ∈ s i
    theorem clusterPt_iff_forall_mem_closure {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :
    ClusterPt x F ↔ βˆ€ s ∈ F, x ∈ closure s
    @[simp]
    theorem clusterPt_lift'_closure_iff {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :
    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 x β†’ s ∈ u β†’ x ∈ s
    theorem isClosed_iff_nhds {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsClosed s ↔ βˆ€ (x : X), (βˆ€ U ∈ nhds x, Set.Nonempty (U ∩ s)) β†’ x ∈ s
    theorem isClosed_iff_forall_filter {X : Type u} {s : Set X} [TopologicalSpace X] :
    IsClosed s ↔ βˆ€ (x : X) (F : Filter X), Filter.NeBot F β†’ F ≀ Filter.principal s β†’ F ≀ nhds x β†’ x ∈ s
    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) :
    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) :

    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) :

    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) :
    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 Ξ±} [Filter.NeBot b] (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 Ξ±} [Filter.NeBot b] (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 : βˆ€ a βˆ‰ s, 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) :

    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 : X β†’ Y}, Continuous f ↔ βˆ€ (s : Set Y), IsOpen s β†’ IsOpen (f ⁻¹' s)
    theorem IsOpen.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} (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 : X β†’ Y} {g : X β†’ Y} (h : βˆ€ (x : X), f x = g x) :
    theorem Continuous.congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} {g : X β†’ Y} (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 : X β†’ Y} {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 : X β†’ Y} {x : X} :
    ContinuousAt f x ↔ βˆ€ A ∈ nhds (f x), f ⁻¹' A ∈ nhds x
    theorem continuousAt_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} {x : X} {g : X β†’ Y} (h : f =αΆ [nhds x] g) :
    theorem ContinuousAt.congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} {x : X} {g : X β†’ Y} (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 : X β†’ Y} {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 : X β†’ Y} {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 : X β†’ Mβ‚€} :

    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 : X β†’ Y} {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

    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 : X β†’ Y} {g : Y β†’ Z} (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 : X β†’ Y} {g : Y β†’ Z} (hg : Continuous g) (hf : Continuous f) :
    Continuous fun (x : X) => g (f x)
    theorem Continuous.iterate {X : Type u_1} [TopologicalSpace X] {f : X β†’ X} (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 : X β†’ Y} {x : X} {g : Y β†’ Z} (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 : X β†’ Y} {g : Y β†’ Z} {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 : X β†’ Y} {x : X} {y : Y} {g : Y β†’ Z} (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 : X β†’ Y} (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 : X β†’ Y} (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 : X β†’ Y} {x : X} (h : Continuous f) :
    theorem continuous_iff_continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} :
    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 : X β†’ Y} {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 : X β†’ Y} (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 : X β†’ X} (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 : X β†’ Y} :
    Continuous f ↔ βˆ€ (s : Set Y), IsClosed s β†’ IsClosed (f ⁻¹' s)
    theorem IsClosed.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} (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 : X β†’ Y} {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 : X β†’ Y} {x : X} :
    ContinuousAt f x ↔ βˆ€ (g : Ultrafilter X), ↑g ≀ nhds x β†’ Filter.Tendsto f (↑g) (nhds (f x))
    theorem continuous_iff_ultrafilter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} :
    Continuous f ↔ βˆ€ (x : X) (g : Ultrafilter X), ↑g ≀ nhds x β†’ Filter.Tendsto f (↑g) (nhds (f x))
    theorem Continuous.closure_preimage_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} (hf : Continuous f) (t : Set Y) :
    theorem Continuous.frontier_preimage_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} (hf : Continuous f) (t : Set Y) :
    theorem Set.MapsTo.closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} {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 : X β†’ Y} {s : Set X} (h : Continuous f) :

    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 : X β†’ Y} {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 : X β†’ Y} {s : Set X} (h : Continuous f) :
    theorem map_mem_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} {s : Set X} {x : X} {t : Set Y} (hf : Continuous f) (hx : x ∈ closure s) (ht : Set.MapsTo f s t) :
    theorem Set.MapsTo.closure_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} {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 : X β†’ Y} (hf : Continuous f) {l : Filter X} {l' : Filter Y} (h : Filter.Tendsto f l l') :
    Filter.Tendsto f (Filter.lift' l closure) (Filter.lift' l' closure)
    theorem tendsto_lift'_closure_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X β†’ Y} (hf : Continuous f) (x : X) :
    Filter.Tendsto f (Filter.lift' (nhds x) closure) (Filter.lift' (nhds (f x)) 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
    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 : X β†’ Y} (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 : X β†’ Y} (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) :

    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 : X β†’ Y} (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 : Y β†’ Z} {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 : Set.Nonempty s) :
      βˆƒ (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