Basic theory of topological spaces.

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

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

Notation

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

• 𝓝 x: the filter nhds x of neighborhoods of a point x;
• 𝓟 s: the principal filter of a set s;
• 𝓝[s] x: the filter nhdsWithin x s of neighborhoods of a point x within a set s;
• 𝓝[≠] x: the filter nhdsWithin x {x}ᶜ of punctured neighborhoods of x.

Implementation notes

Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in .

References

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

Tags

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

Topological spaces

def TopologicalSpace.ofClosed {X : Type u} (T : Set (Set X)) (empty_mem : ∅ ∈ T) (sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T) (union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T) : TopologicalSpace X

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

Equations

• TopologicalSpace.ofClosed T empty_mem sInter_mem union_mem = { IsOpen := fun (X_1 : Set X) => X_1ᶜ ∈ T, isOpen_univ := ⋯, isOpen_inter := ⋯, isOpen_sUnion := ⋯ }

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)} : IsOpen s ↔ 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_fold {X : Type u} {s : Set X} {t : TopologicalSpace X} : TopologicalSpace.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)

@[simp]

theorem isOpen_empty {X : Type u} [TopologicalSpace X] : IsOpen ∅

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}

@[simp]

theorem isOpen_compl_iff {X : Type u} {s : Set X} [TopologicalSpace X] : IsOpen sᶜ ↔ IsClosed s

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_empty {X : Type u} [TopologicalSpace X] : IsClosed ∅

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

@[simp]

theorem isClosed_compl_iff {X : Type u} [TopologicalSpace X] {s : Set X} : IsClosed sᶜ ↔ IsOpen s

theorem IsOpen.isClosed_compl {X : Type u} [TopologicalSpace X] {s : Set X} : IsOpen s → IsClosed sᶜ

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] : IsOpen (interior s)

theorem interior_subset {X : Type u} {s : Set X} [TopologicalSpace X] : interior s ⊆ s

theorem interior_maximal {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : t ⊆ s) (h₂ : IsOpen t) : t ⊆ interior s

theorem IsOpen.interior_eq {X : Type u} {s : Set X} [TopologicalSpace X] (h : IsOpen s) : interior s = s

theorem interior_eq_iff_isOpen {X : Type u} {s : Set X} [TopologicalSpace X] : interior s = s ↔ IsOpen s

theorem subset_interior_iff_isOpen {X : Type u} {s : Set X} [TopologicalSpace X] : s ⊆ interior s ↔ IsOpen s

theorem IsOpen.subset_interior_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : IsOpen s) : s ⊆ interior t ↔ s ⊆ t

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) : interior s ⊆ interior t

@[simp]

theorem interior_empty {X : Type u} [TopologicalSpace X] : interior ∅ = ∅

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

theorem interior_interior {X : Type u} {s : Set X} [TopologicalSpace X] : interior (interior s) = interior s

@[simp]

theorem interior_inter {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] : interior (s ∩ t) = interior s ∩ interior t

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 = ∅) : interior (s ∪ t) = interior s

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.lift'_interior_le {X : Type u} [TopologicalSpace X] (l : Filter X) : Filter.lift' l interior ≤ l

theorem Filter.HasBasis.lift'_interior_eq_self {X : Type u} {ι : Sort w} [TopologicalSpace X] {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : 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] : IsClosed (closure s)

theorem subset_closure {X : Type u} {s : Set X} [TopologicalSpace X] : s ⊆ closure s

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) : closure s ⊆ t

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

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

theorem IsClosed.closure_eq {X : Type u} {s : Set X} [TopologicalSpace X] (h : IsClosed s) : closure s = s

theorem IsClosed.closure_subset {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) : closure s ⊆ s

theorem IsClosed.closure_subset_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h₁ : IsClosed t) : closure s ⊆ t ↔ s ⊆ t

theorem IsClosed.mem_iff_closure_subset {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) : x ∈ s ↔ closure {x} ⊆ s

theorem closure_mono {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : s ⊆ t) : closure s ⊆ closure t

theorem monotone_closure (X : Type u_3) [TopologicalSpace X] : Monotone closure

theorem diff_subset_closure_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] : s \ t ⊆ closure t ↔ s ⊆ closure t

theorem closure_inter_subset_inter_closure {X : Type u} [TopologicalSpace X] (s : Set X) (t : Set X) : closure (s ∩ t) ⊆ closure s ∩ closure t

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

theorem closure_eq_iff_isClosed {X : Type u} {s : Set X} [TopologicalSpace X] : closure s = s ↔ IsClosed s

theorem closure_subset_iff_isClosed {X : Type u} {s : Set X} [TopologicalSpace X] : closure s ⊆ s ↔ IsClosed s

@[simp]

theorem closure_empty {X : Type u} [TopologicalSpace X] : closure ∅ = ∅

@[simp]

theorem closure_empty_iff {X : Type u} [TopologicalSpace X] (s : Set X) : closure s = ∅ ↔ s = ∅

@[simp]

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

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

Alias of the forward direction of closure_nonempty_iff.

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

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] : closure (closure s) = closure s

theorem closure_eq_compl_interior_compl {X : Type u} {s : Set X} [TopologicalSpace X] : closure s = (interior sᶜ)ᶜ

@[simp]

theorem closure_union {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] : closure (s ∪ t) = closure s ∪ closure t

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)

theorem interior_subset_closure {X : Type u} {s : Set X} [TopologicalSpace X] : interior s ⊆ closure s

@[simp]

theorem interior_compl {X : Type u} {s : Set X} [TopologicalSpace X] : interior sᶜ = (closure s)ᶜ

@[simp]

theorem closure_compl {X : Type u} {s : Set X} [TopologicalSpace X] : closure sᶜ = (interior s)ᶜ

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 closure_inter_open_nonempty_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsOpen t) : Set.Nonempty (closure s ∩ t) ↔ Set.Nonempty (s ∩ t)

theorem Filter.le_lift'_closure {X : Type u} [TopologicalSpace X] (l : Filter X) : l ≤ Filter.lift' l closure

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

@[simp]

theorem Filter.lift'_closure_eq_bot {X : Type u} [TopologicalSpace X] {l : Filter X} : 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.

theorem interior_eq_empty_iff_dense_compl {X : Type u} {s : Set X} [TopologicalSpace X] : interior s = ∅ ↔ Dense sᶜ

theorem Dense.interior_compl {X : Type u} {s : Set X} [TopologicalSpace X] (h : Dense s) : interior sᶜ = ∅

@[simp]

theorem dense_closure {X : Type u} {s : Set X} [TopologicalSpace X] : Dense (closure s) ↔ Dense s

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_iff {X : Type u} {s : Set X} [TopologicalSpace X] (hs : Dense s) : Set.Nonempty s ↔ Nonempty X

theorem Dense.nonempty {X : Type u} {s : Set X} [TopologicalSpace X] [h : Nonempty X] (hs : Dense s) : Set.Nonempty s

theorem Dense.mono {X : Type u} {s₁ : Set X} {s₂ : Set X} [TopologicalSpace X] (h : s₁ ⊆ s₂) (hd : Dense s₁) : Dense s₂

theorem dense_compl_singleton_iff_not_open {X : Type u} {x : X} [TopologicalSpace X] : Dense {x}ᶜ ↔ ¬IsOpen {x}

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

Frontier of a set

@[simp]

theorem closure_diff_interior {X : Type u} [TopologicalSpace X] (s : Set X) : closure s \ interior s = frontier s

theorem disjoint_interior_frontier {X : Type u} {s : Set X} [TopologicalSpace X] : Disjoint (interior s) (frontier s)

Interior and frontier are disjoint.

@[simp]

theorem closure_diff_frontier {X : Type u} [TopologicalSpace X] (s : Set X) : closure s \ frontier s = interior s

@[simp]

theorem self_diff_frontier {X : Type u} [TopologicalSpace X] (s : Set X) : s \ frontier s = interior s

theorem frontier_eq_closure_inter_closure {X : Type u} {s : Set X} [TopologicalSpace X] : frontier s = closure s ∩ closure sᶜ

theorem frontier_subset_closure {X : Type u} {s : Set X} [TopologicalSpace X] : frontier s ⊆ closure s

theorem IsClosed.frontier_subset {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) : frontier s ⊆ s

theorem frontier_closure_subset {X : Type u} {s : Set X} [TopologicalSpace X] : frontier (closure s) ⊆ frontier s

theorem frontier_interior_subset {X : Type u} {s : Set X} [TopologicalSpace X] : frontier (interior s) ⊆ frontier s

@[simp]

theorem frontier_compl {X : Type u} [TopologicalSpace X] (s : Set X) : frontier sᶜ = frontier s

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 = ∅

@[simp]

theorem frontier_empty {X : Type u} [TopologicalSpace X] : frontier ∅ = ∅

theorem frontier_inter_subset {X : Type u} [TopologicalSpace X] (s : Set X) (t : Set X) : frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t

theorem frontier_union_subset {X : Type u} [TopologicalSpace X] (s : Set X) (t : Set X) : frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t

theorem IsClosed.frontier_eq {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) : frontier s = s \ interior s

theorem IsOpen.frontier_eq {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsOpen s) : frontier s = closure s \ s

theorem IsOpen.inter_frontier_eq {X : Type u} {s : Set X} [TopologicalSpace X] (hs : IsOpen s) : s ∩ frontier s = ∅

theorem isClosed_frontier {X : Type u} {s : Set X} [TopologicalSpace X] : IsClosed (frontier s)

The frontier of a set is closed.

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

The frontier of a closed set has no interior point.

theorem closure_eq_interior_union_frontier {X : Type u} [TopologicalSpace X] (s : Set X) : closure s = interior s ∪ frontier s

theorem closure_eq_self_union_frontier {X : Type u} [TopologicalSpace X] (s : Set X) : closure s = s ∪ frontier s

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

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

theorem frontier_eq_inter_compl_interior {X : Type u} {s : Set X} [TopologicalSpace X] : frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ

theorem compl_frontier_eq_union_interior {X : Type u} {s : Set X} [TopologicalSpace X] : (frontier s)ᶜ = interior s ∪ interior sᶜ

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) : nhds x ≤ f

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

theorem mem_nhds_iff {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : s ∈ nhds x ↔ ∃ 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 mem_interior_iff_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ interior s ↔ s ∈ nhds 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) : s ∈ nhds x

theorem IsOpen.mem_nhds_iff {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsOpen s) : s ∈ nhds x ↔ x ∈ s

theorem IsClosed.compl_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] (hs : IsClosed s) (hx : x ∉ s) : sᶜ ∈ nhds x

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] : Filter.NeBot (nhds 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) : Filter.Tendsto f l (nhds 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) : Filter.Tendsto f l (nhds 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) : Filter.NeBot (nhds 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_iff_not_disjoint {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} : ClusterPt x F ↔ ¬Disjoint (nhds x) F

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] : ClusterPt x f

theorem ClusterPt.of_le_nhds' {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} (H : f ≤ nhds x) (_hf : Filter.NeBot f) : ClusterPt x f

theorem ClusterPt.of_nhds_le {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} (H : nhds x ≤ f) : ClusterPt 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) : ClusterPt x g

theorem ClusterPt.of_inf_left {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} {g : Filter X} (H : ClusterPt x (f ⊓ g)) : ClusterPt x f

theorem ClusterPt.of_inf_right {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} {g : Filter X} (H : ClusterPt x (f ⊓ g)) : ClusterPt x 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) : MapClusterPt x F u ↔ ClusterPt x (Filter.map u F)

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_comp {X : Type u_3} {α : Type u_4} {β : Type u_5} {x : X} [TopologicalSpace X] {F : Filter α} {φ : α → β} {u : β → X} : MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (Filter.map φ F) u

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)) : MapClusterPt x F u

theorem acc_iff_cluster {X : Type u} [TopologicalSpace X] (x : X) (F : Filter X) : AccPt x F ↔ ClusterPt x (Filter.principal {x}ᶜ ⊓ F)

theorem acc_principal_iff_cluster {X : Type u} [TopologicalSpace X] (x : X) (C : Set X) : AccPt x (Filter.principal C) ↔ ClusterPt x (Filter.principal (C \ {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}

theorem interior_eq_nhds {X : Type u} {s : Set X} [TopologicalSpace X] : interior s = {x : X | nhds x ≤ Filter.principal s}

@[simp]

theorem interior_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : interior s ∈ nhds x ↔ s ∈ nhds 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 isOpen_singleton_iff_nhds_eq_pure {X : Type u} [TopologicalSpace X] (x : X) : IsOpen {x} ↔ nhds x = pure x

theorem isOpen_singleton_iff_punctured_nhds {X : Type u} [TopologicalSpace X] (x : X) : IsOpen {x} ↔ nhdsWithin x {x}ᶜ = ⊥

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.

theorem mem_closure_iff_clusterPt {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ closure s ↔ ClusterPt x (Filter.principal s)

theorem mem_closure_iff_nhds_ne_bot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥

@[deprecated mem_closure_iff_nhds_ne_bot]

theorem mem_closure_iff_nhds_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥

Alias of mem_closure_iff_nhds_ne_bot.

theorem mem_closure_iff_nhdsWithin_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ closure s ↔ Filter.NeBot (nhdsWithin x s)

theorem not_mem_closure_iff_nhdsWithin_eq_bot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∉ closure s ↔ nhdsWithin x s = ⊥

theorem dense_compl_singleton {X : Type u} [TopologicalSpace X] (x : X) [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 {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]

theorem interior_singleton {X : Type u} [TopologicalSpace X] (x : X) [Filter.NeBot (nhdsWithin x {x}ᶜ)] : interior {x} = ∅

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

theorem not_isOpen_singleton {X : Type u} [TopologicalSpace X] (x : X) [Filter.NeBot (nhdsWithin x {x}ᶜ)] : ¬IsOpen {x}

theorem closure_eq_cluster_pts {X : Type u} {s : Set X} [TopologicalSpace X] : closure s = {a : X | ClusterPt a (Filter.principal s)}

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_comap_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ closure s ↔ Filter.NeBot (Filter.comap Subtype.val (nhds x))

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

theorem clusterPt_iff_lift'_closure {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} : ClusterPt x F ↔ pure x ≤ Filter.lift' F closure

theorem clusterPt_iff_lift'_closure' {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} : ClusterPt x F ↔ Filter.NeBot (Filter.lift' F closure ⊓ pure x)

@[simp]

theorem clusterPt_lift'_closure_iff {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} : ClusterPt x (Filter.lift' F closure) ↔ ClusterPt x F

theorem mem_closure_iff_ultrafilter {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] : x ∈ closure s ↔ ∃ (u : Ultrafilter X), s ∈ u ∧ ↑u ≤ nhds x

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

theorem isClosed_iff_clusterPt {X : Type u} {s : Set X} [TopologicalSpace X] : IsClosed s ↔ ∀ (a : X), ClusterPt a (Filter.principal s) → a ∈ s

theorem isClosed_iff_ultrafilter {X : Type u} {s : Set X} [TopologicalSpace X] : IsClosed s ↔ ∀ (x : X) (u : Ultrafilter X), ↑u ≤ nhds 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 IsClosed.interior_union_left {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] : IsClosed s → interior (s ∪ t) ⊆ s ∪ interior t

theorem IsClosed.interior_union_right {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsClosed t) : interior (s ∪ t) ⊆ interior s ∪ t

theorem IsOpen.inter_closure {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsOpen s) : s ∩ closure t ⊆ closure (s ∩ t)

theorem IsOpen.closure_inter {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsOpen t) : closure s ∩ t ⊆ closure (s ∩ t)

theorem Dense.open_subset_closure_inter {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (hs : Dense s) (ht : IsOpen t) : t ⊆ closure (t ∩ s)

theorem mem_closure_of_mem_closure_union {X : Type u} {x : X} {s₁ : Set X} {s₂ : Set X} [TopologicalSpace X] (h : x ∈ closure (s₁ ∪ s₂)) (h₁ : s₁ᶜ ∈ nhds x) : x ∈ closure s₂

theorem Dense.inter_of_isOpen_left {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (hs : Dense s) (ht : Dense t) (hso : IsOpen s) : Dense (s ∩ t)

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

theorem Dense.inter_of_isOpen_right {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (hs : Dense s) (ht : Dense t) (hto : IsOpen t) : Dense (s ∩ t)

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

theorem Dense.inter_nhds_nonempty {X : Type u} {x : X} {s : Set X} {t : Set X} [TopologicalSpace X] (hs : Dense s) (ht : t ∈ nhds x) : Set.Nonempty (s ∩ t)

theorem closure_diff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] : closure s \ closure t ⊆ closure (s \ t)

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)) : x ∈ closure s

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) : x ∈ closure 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) : Filter.Tendsto f (l ⊓ Filter.principal s) (nhds x) ↔ Filter.Tendsto f l (nhds x)

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

Limits of filters in topological spaces

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

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

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

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

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) : IsOpen (f ⁻¹' 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) : Continuous f ↔ Continuous g

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

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) : ContinuousAt f x ↔ ContinuousAt g x

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) : ContinuousAt g x

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)) : f ⁻¹' t ∈ nhds 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₀} : f =ᶠ[nhds x] 0 ↔ x ∉ closure (Function.support f)

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

theorem preimage_interior_subset_interior_preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {t : Set Y} (hf : Continuous f) : f ⁻¹' interior t ⊆ interior (f ⁻¹' t)

See also interior_preimage_subset_preimage_interior.

theorem continuous_id {X : Type u_1} [TopologicalSpace X] : Continuous id

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) : Continuous (g ∘ 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 : ℕ) : 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) : ContinuousAt (g ∘ 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) : ContinuousAt (g ∘ f) x

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) : Filter.Tendsto f (nhds x) (nhds 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) : ContinuousAt f x

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) : ContinuousAt f x

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

theorem continuousAt_id {X : Type u_1} [TopologicalSpace X] {x : X} : ContinuousAt id 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 : ℕ) : ContinuousAt f^[n] x

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) : IsClosed (f ⁻¹' 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) : closure (f ⁻¹' t) ⊆ f ⁻¹' closure t

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) : frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t

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) : Set.MapsTo f (closure s) (closure t)

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) : f '' closure s ⊆ closure (f '' s)

See also IsClosedMap.closure_image_eq_of_continuous.

theorem closure_image_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} (h : Continuous f) : closure (f '' closure s) = closure (f '' s)

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) : closure s ⊆ f ⁻¹' closure (f '' s)

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) : f x ∈ closure 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) : Set.MapsTo f (closure s) 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) : DenseRange f

A surjective map has dense range.

theorem denseRange_id {X : Type u_1} [TopologicalSpace X] : DenseRange id

theorem denseRange_iff_closure_range {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} : DenseRange f ↔ closure (Set.range f) = Set.univ

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) : Set.range f ⊆ closure (f '' 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) : s ⊆ closure (f '' (f ⁻¹' s))

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

theorem DenseRange.dense_of_mapsTo {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {s : Set X} {f : X → Y} (hf' : DenseRange f) (hf : Continuous f) (hs : Dense s) {t : Set Y} (ht : Set.MapsTo f s t) : Dense 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) : DenseRange (g ∘ f)

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) : Nonempty α ↔ Nonempty X

theorem DenseRange.nonempty {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} [h : Nonempty X] (hf : DenseRange f) : Nonempty α

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

• DenseRange.some hf x = Classical.choice ⋯

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