Basic theory of topological spaces.

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

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

Notation

• 𝓝 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 (Set.Iic x) of left-neighborhoods of x;
• 𝓝[≥] x: the filter nhdsWithin x (Set.Ici x) of right-neighborhoods of x;
• 𝓝[<] x: the filter nhdsWithin x (Set.Iio x) of punctured left-neighborhoods of x;
• 𝓝[>] x: the filter nhdsWithin x (Set.Ioi x) of punctured right-neighborhoods of x;
• 𝓝[≠] x: the filter nhdsWithin x {x}ᶜ of punctured neighborhoods of x.

Implementation notes

Topology in mathlib heavily uses filters (even more than in Bourbaki). See explanations in https://leanprover-community.github.io/theories/topology.html.

References

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

Tags

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

Topological spaces

class TopologicalSpace (α : Type u) : Type u

• IsOpen : Set α → Prop

  A predicate saying that a set is an open set. Use IsOpen in the root namespace instead.

• isOpen_univ : TopologicalSpace.IsOpen Set.univ

  The set representing the whole space is an open set. Use isOpen_univ in the root namespace instead.

• isOpen_inter : ∀ (s_1 t : Set α), TopologicalSpace.IsOpen s_1 → TopologicalSpace.IsOpen t → TopologicalSpace.IsOpen (s_1 ∩ t)

  The intersection of two open sets is an open set. Use IsOpen.inter instead.

• isOpen_sUnion : ∀ (s_1 : Set (Set α)), (∀ (t : Set α), t ∈ s_1 → TopologicalSpace.IsOpen t) → TopologicalSpace.IsOpen (⋃₀ s_1)

  The union of a family of open sets is an open set. Use isOpen_sUnion in the root namespace instead.

A topology on α.

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

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

Equations

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

def IsOpen {α : Type u} [TopologicalSpace α] : Set α → Prop

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

Equations

• IsOpen = TopologicalSpace.IsOpen

def Topology.IsOpen_of : Lean.ParserDescr

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

Equations

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

theorem isOpen_mk {α : Type u} {p : Set α → Prop} {h₁ : p Set.univ} {h₂ : (s t : Set α) → p s → p t → p (s ∩ t)} {h₃ : (s : Set (Set α)) → ((t : Set α) → t ∈ s → p t) → p (⋃₀ s)} {s : Set α} : IsOpen s ↔ p s

theorem TopologicalSpace.ext {α : Type u} {f : TopologicalSpace α} {g : TopologicalSpace α} : IsOpen = IsOpen → f = g

@[simp]

theorem isOpen_univ {α : Type u} [TopologicalSpace α] : IsOpen Set.univ

theorem IsOpen.inter {α : Type u} {s₁ : Set α} {s₂ : Set α} [TopologicalSpace α] (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∩ s₂)

theorem isOpen_sUnion {α : Type u} [TopologicalSpace α] {s : Set (Set α)} (h : ∀ (t : Set α), t ∈ s → IsOpen t) : IsOpen (⋃₀ s)

theorem TopologicalSpace.ext_iff {α : Type u} {t : TopologicalSpace α} {t' : TopologicalSpace α} : t = t' ↔ ∀ (s : Set α), IsOpen s ↔ IsOpen s

theorem isOpen_fold {α : Type u} {s : Set α} {t : TopologicalSpace α} : TopologicalSpace.IsOpen s = IsOpen s

theorem isOpen_iUnion {α : Type u} {ι : Sort w} [TopologicalSpace α] {f : ι → Set α} (h : ∀ (i : ι), IsOpen (f i)) : IsOpen (⋃ (i : ι), f i)

theorem isOpen_biUnion {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set β} {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsOpen (f i)) : IsOpen (⋃ (i : β) (_ : i ∈ s), f i)

theorem IsOpen.union {α : Type u} {s₁ : Set α} {s₂ : Set α} [TopologicalSpace α] (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∪ s₂)

@[simp]

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

theorem Set.Finite.isOpen_sInter {α : Type u} [TopologicalSpace α] {s : Set (Set α)} (hs : Set.Finite s) : (∀ (t : Set α), t ∈ s → IsOpen t) → IsOpen (⋂₀ s)

theorem Set.Finite.isOpen_biInter {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set β} {f : β → Set α} (hs : Set.Finite s) (h : ∀ (i : β), i ∈ s → IsOpen (f i)) : IsOpen (⋂ (i : β) (_ : i ∈ s), f i)

theorem isOpen_iInter_of_finite {α : Type u} {ι : Sort w} [TopologicalSpace α] [Finite ι] {s : ι → Set α} (h : ∀ (i : ι), IsOpen (s i)) : IsOpen (⋂ (i : ι), s i)

theorem isOpen_biInter_finset {α : Type u} {β : Type v} [TopologicalSpace α] {s : Finset β} {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsOpen (f i)) : IsOpen (⋂ (i : β) (_ : i ∈ s), f i)

@[simp]

theorem isOpen_const {α : Type u} [TopologicalSpace α] {p : Prop} : IsOpen {_a | p}

theorem IsOpen.and {α : Type u} {p₁ : α → Prop} {p₂ : α → Prop} [TopologicalSpace α] : IsOpen {a | p₁ a} → IsOpen {a | p₂ a} → IsOpen {a | p₁ a ∧ p₂ a}

class IsClosed {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

• isOpen_compl : IsOpen s✝ᶜ

  The complement of a closed set is an open set.

A set is closed if its complement is open

def Topology.IsClosed_of : Lean.ParserDescr

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

Equations

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

@[simp]

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

theorem isClosed_const {α : Type u} [TopologicalSpace α] {p : Prop} : IsClosed {_a | p}

@[simp]

theorem isClosed_empty {α : Type u} [TopologicalSpace α] : IsClosed ∅

@[simp]

theorem isClosed_univ {α : Type u} [TopologicalSpace α] : IsClosed Set.univ

theorem IsClosed.union {α : Type u} {s₁ : Set α} {s₂ : Set α} [TopologicalSpace α] : IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)

theorem isClosed_sInter {α : Type u} [TopologicalSpace α] {s : Set (Set α)} : (∀ (t : Set α), t ∈ s → IsClosed t) → IsClosed (⋂₀ s)

theorem isClosed_iInter {α : Type u} {ι : Sort w} [TopologicalSpace α] {f : ι → Set α} (h : ∀ (i : ι), IsClosed (f i)) : IsClosed (⋂ (i : ι), f i)

theorem isClosed_biInter {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set β} {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsClosed (f i)) : IsClosed (⋂ (i : β) (_ : i ∈ s), f i)

@[simp]

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

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

Alias of the reverse direction of isClosed_compl_iff.

theorem IsOpen.sdiff {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (h₁ : IsOpen s) (h₂ : IsClosed t) : IsOpen (s \ t)

theorem IsClosed.inter {α : Type u} {s₁ : Set α} {s₂ : Set α} [TopologicalSpace α] (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) : IsClosed (s₁ ∩ s₂)

theorem IsClosed.sdiff {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (h₁ : IsClosed s) (h₂ : IsOpen t) : IsClosed (s \ t)

theorem Set.Finite.isClosed_biUnion {α : Type u} {β : Type v} [TopologicalSpace α] {s : Set β} {f : β → Set α} (hs : Set.Finite s) (h : ∀ (i : β), i ∈ s → IsClosed (f i)) : IsClosed (⋃ (i : β) (_ : i ∈ s), f i)

theorem isClosed_biUnion_finset {α : Type u} {β : Type v} [TopologicalSpace α] {s : Finset β} {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsClosed (f i)) : IsClosed (⋃ (i : β) (_ : i ∈ s), f i)

theorem isClosed_iUnion_of_finite {α : Type u} {ι : Sort w} [TopologicalSpace α] [Finite ι] {s : ι → Set α} (h : ∀ (i : ι), IsClosed (s i)) : IsClosed (⋃ (i : ι), s i)

theorem isClosed_imp {α : Type u} [TopologicalSpace α] {p : α → Prop} {q : α → Prop} (hp : IsOpen {x | p x}) (hq : IsClosed {x | q x}) : IsClosed {x | p x → q x}

theorem IsClosed.not {α : Type u} {p : α → Prop} [TopologicalSpace α] : IsClosed {a | p a} → IsOpen {a | ¬p a}

Interior of a set

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

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

Equations

• interior s = ⋃₀ {t | IsOpen t ∧ t ⊆ s}

theorem mem_interior {α : Type u} [TopologicalSpace α] {s : Set α} {x : α} : x ∈ interior s ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t

@[simp]

theorem isOpen_interior {α : Type u} [TopologicalSpace α] {s : Set α} : IsOpen (interior s)

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

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

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

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

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

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

theorem subset_interior_iff {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} : t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s

theorem interior_subset_iff {α : Type u} {s : Set α} {t : Set α} [TopologicalSpace α] : interior s ⊆ t ↔ ∀ (U : Set α), IsOpen U → U ⊆ s → U ⊆ t

theorem interior_mono {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (h : s ⊆ t) : interior s ⊆ interior t

@[simp]

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

@[simp]

theorem interior_univ {α : Type u} [TopologicalSpace α] : interior Set.univ = Set.univ

@[simp]

theorem interior_eq_univ {α : Type u} [TopologicalSpace α] {s : Set α} : interior s = Set.univ ↔ s = Set.univ

@[simp]

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

@[simp]

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

@[simp]

theorem Finset.interior_iInter {α : Type u} [TopologicalSpace α] {ι : Type u_1} (s : Finset ι) (f : ι → Set α) : interior (⋂ (i : ι) (_ : i ∈ s), f i) = ⋂ (i : ι) (_ : i ∈ s), interior (f i)

@[simp]

theorem interior_iInter_of_finite {α : Type u} [TopologicalSpace α] {ι : Type u_1} [Finite ι] (f : ι → Set α) : interior (⋂ (i : ι), f i) = ⋂ (i : ι), interior (f i)

theorem interior_union_isClosed_of_interior_empty {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (h₁ : IsClosed s) (h₂ : interior t = ∅) : interior (s ∪ t) = interior s

theorem isOpen_iff_forall_mem_open {α : Type u} {s : Set α} [TopologicalSpace α] : IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t

theorem interior_iInter_subset {α : Type u} {ι : Sort w} [TopologicalSpace α] (s : ι → Set α) : interior (⋂ (i : ι), s i) ⊆ ⋂ (i : ι), interior (s i)

theorem interior_Inter₂_subset {α : Type u} {ι : Sort w} [TopologicalSpace α] (p : ι → Sort u_1) (s : (i : ι) → p i → Set α) : interior (⋂ (i : ι) (j : p i), s i j) ⊆ ⋂ (i : ι) (j : p i), interior (s i j)

theorem interior_sInter_subset {α : Type u} [TopologicalSpace α] (S : Set (Set α)) : interior (⋂₀ S) ⊆ ⋂ (s : Set α) (_ : s ∈ S), interior s

Closure of a set

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

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

Equations

• closure s = ⋂₀ {t | IsClosed t ∧ s ⊆ t}

def Topology.closure_of : Lean.ParserDescr

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

Equations

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

@[simp]

theorem isClosed_closure {α : Type u} [TopologicalSpace α] {s : Set α} : IsClosed (closure s)

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

theorem not_mem_of_not_mem_closure {α : Type u} [TopologicalSpace α] {s : Set α} {P : α} (hP : ¬P ∈ closure s) : ¬P ∈ s

theorem closure_minimal {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (h₁ : s ⊆ t) (h₂ : IsClosed t) : closure s ⊆ t

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

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

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

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

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

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

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

theorem monotone_closure (α : Type u_1) [TopologicalSpace α] : Monotone closure

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of closure_nonempty_iff.

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

Alias of the forward direction of closure_nonempty_iff.

@[simp]

theorem closure_univ {α : Type u} [TopologicalSpace α] : closure Set.univ = Set.univ

@[simp]

theorem closure_closure {α : Type u} [TopologicalSpace α] {s : Set α} : closure (closure s) = closure s

@[simp]

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

@[simp]

theorem Finset.closure_biUnion {α : Type u} [TopologicalSpace α] {ι : Type u_1} (s : Finset ι) (f : ι → Set α) : closure (⋃ (i : ι) (_ : i ∈ s), f i) = ⋃ (i : ι) (_ : i ∈ s), closure (f i)

@[simp]

theorem closure_Union_of_finite {α : Type u} [TopologicalSpace α] {ι : Type u_1} [Finite ι] (f : ι → Set α) : closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)

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

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

@[simp]

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

@[simp]

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

theorem mem_closure_iff {α : Type u} [TopologicalSpace α] {s : Set α} {a : α} : a ∈ closure s ↔ ∀ (o : Set α), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)

theorem closure_inter_open_nonempty_iff {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} (h : IsOpen t) : Set.Nonempty (closure s ∩ t) ↔ Set.Nonempty (s ∩ t)

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

theorem Filter.HasBasis.lift'_closure {α : Type u} {ι : Sort w} [TopologicalSpace α] {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) : Filter.HasBasis (Filter.lift' l closure) p fun i => closure (s i)

theorem Filter.HasBasis.lift'_closure_eq_self {α : Type u} {ι : Sort w} [TopologicalSpace α] {l : Filter α} {p : ι → Prop} {s : ι → Set α} (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 {α : Type u} [TopologicalSpace α] {l : Filter α} : Filter.lift' l closure = ⊥ ↔ l = ⊥

def Dense {α : Type u} [TopologicalSpace α] (s : Set α) : Prop

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

Equations

• Dense s = ∀ (x : α), x ∈ closure s

theorem dense_iff_closure_eq {α : Type u} [TopologicalSpace α] {s : Set α} : Dense s ↔ closure s = Set.univ

theorem Dense.closure_eq {α : Type u} [TopologicalSpace α] {s : Set α} : Dense s → closure s = Set.univ

Alias of the forward direction of dense_iff_closure_eq.

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

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

@[simp]

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

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

theorem Dense.closure {α : Type u} [TopologicalSpace α] {s : Set α} : 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 {α : Type u} [TopologicalSpace α] {s : Set α} : 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 {α : Type u} [TopologicalSpace α] : Dense Set.univ

theorem dense_iff_inter_open {α : Type u} [TopologicalSpace α] {s : Set α} : Dense s ↔ ∀ (U : Set α), 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 {α : Type u} [TopologicalSpace α] {s : Set α} : Dense s → ∀ (U : Set α), 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 {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Dense s) {U : Set α} (ho : IsOpen U) (hne : Set.Nonempty U) : ∃ x, x ∈ s ∧ x ∈ U

theorem Dense.nonempty_iff {α : Type u} [TopologicalSpace α] {s : Set α} (hs : Dense s) : Set.Nonempty s ↔ Nonempty α

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

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

theorem dense_compl_singleton_iff_not_open {α : Type u} [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

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

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

Equations

• frontier s = closure s \ interior s

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

@[simp]

theorem frontier_univ {α : Type u} [TopologicalSpace α] : frontier Set.univ = ∅

@[simp]

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

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

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

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

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

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

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

The frontier of a set is closed.

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

The frontier of a closed set has no interior point.

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

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

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

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

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

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

Neighborhoods

theorem nhds_def {α : Type u_1} [TopologicalSpace α] (a : α) : nhds a = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), Filter.principal s

@[irreducible]

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

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

Equations

• @nhds = wrapped✝.1

def nhdsWithin {α : Type u} [TopologicalSpace α] (a : α) (s : Set α) : Filter α

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

Equations

• nhdsWithin a s = nhds a ⊓ Filter.principal s

def Topology.term𝓝 : Lean.ParserDescr

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

Equations

• Topology.term𝓝 = Lean.ParserDescr.node `Topology.term𝓝 1024 (Lean.ParserDescr.symbol "𝓝")

def Topology.«term𝓝[_]_» : Lean.ParserDescr

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

Equations

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

def Topology.«term𝓝[≠]_» : Lean.ParserDescr

Notation for the filter of punctured neighborhoods of a point.

Equations

• Topology.«term𝓝[≠]_» = Lean.ParserDescr.node `Topology.term𝓝[≠]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[≠] ") (Lean.ParserDescr.cat `term 100))

def Topology.«term𝓝[≥]_» : Lean.ParserDescr

Notation for the filter of right neighborhoods of a point.

Equations

• Topology.«term𝓝[≥]_» = Lean.ParserDescr.node `Topology.term𝓝[≥]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[≥] ") (Lean.ParserDescr.cat `term 100))

def Topology.«term𝓝[≤]_» : Lean.ParserDescr

Notation for the filter of left neighborhoods of a point.

Equations

• Topology.«term𝓝[≤]_» = Lean.ParserDescr.node `Topology.term𝓝[≤]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[≤] ") (Lean.ParserDescr.cat `term 100))

def Topology.«term𝓝[>]_» : Lean.ParserDescr

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

Equations

• Topology.«term𝓝[>]_» = Lean.ParserDescr.node `Topology.term𝓝[>]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[>] ") (Lean.ParserDescr.cat `term 100))

def Topology.«term𝓝[<]_» : Lean.ParserDescr

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

Equations

• Topology.«term𝓝[<]_» = Lean.ParserDescr.node `Topology.term𝓝[<]_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝓝[<] ") (Lean.ParserDescr.cat `term 100))

theorem nhds_def' {α : Type u} [TopologicalSpace α] (a : α) : nhds a = ⨅ (s : Set α) (_ : IsOpen s) (_ : a ∈ s), Filter.principal s

theorem nhds_basis_opens {α : Type u} [TopologicalSpace α] (a : α) : Filter.HasBasis (nhds a) (fun s => a ∈ s ∧ IsOpen s) fun s => s

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

theorem nhds_basis_closeds {α : Type u} [TopologicalSpace α] (a : α) : Filter.HasBasis (nhds a) (fun s => ¬a ∈ s ∧ IsClosed s) compl

theorem le_nhds_iff {α : Type u} [TopologicalSpace α] {f : Filter α} {a : α} : f ≤ nhds a ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f

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

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

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

theorem mem_nhds_iff {α : Type u} [TopologicalSpace α] {a : α} {s : Set α} : s ∈ nhds a ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ a ∈ t

theorem eventually_nhds_iff {α : Type u} [TopologicalSpace α] {a : α} {p : α → Prop} : (∀ᶠ (x : α) in nhds a, p x) ↔ ∃ t, ((x : α) → x ∈ t → p x) ∧ IsOpen t ∧ a ∈ t

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

theorem mem_interior_iff_mem_nhds {α : Type u} [TopologicalSpace α] {s : Set α} {a : α} : a ∈ interior s ↔ s ∈ nhds a

theorem map_nhds {α : Type u} {β : Type v} [TopologicalSpace α] {a : α} {f : α → β} : Filter.map f (nhds a) = ⨅ (s : Set α) (_ : s ∈ {s | a ∈ s ∧ IsOpen s}), Filter.principal (f '' s)

theorem mem_of_mem_nhds {α : Type u} [TopologicalSpace α] {a : α} {s : Set α} : s ∈ nhds a → a ∈ s

theorem Filter.Eventually.self_of_nhds {α : Type u} [TopologicalSpace α] {p : α → Prop} {a : α} (h : ∀ᶠ (y : α) in nhds a, p y) : p a

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

theorem IsOpen.mem_nhds {α : Type u} [TopologicalSpace α] {a : α} {s : Set α} (hs : IsOpen s) (ha : a ∈ s) : s ∈ nhds a

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

theorem IsClosed.compl_mem_nhds {α : Type u} [TopologicalSpace α] {a : α} {s : Set α} (hs : IsClosed s) (ha : ¬a ∈ s) : sᶜ ∈ nhds a

theorem IsOpen.eventually_mem {α : Type u} [TopologicalSpace α] {a : α} {s : Set α} (hs : IsOpen s) (ha : a ∈ s) : ∀ᶠ (x : α) in nhds a, x ∈ s

theorem nhds_basis_opens' {α : Type u} [TopologicalSpace α] (a : α) : Filter.HasBasis (nhds a) (fun s => s ∈ nhds a ∧ IsOpen s) fun x => x

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

theorem exists_open_set_nhds {α : Type u} [TopologicalSpace α] {s : Set α} {U : Set α} (h : ∀ (x : α), x ∈ s → U ∈ nhds x) : ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U

If U is a neighborhood of each point of a set s then it is a neighborhood of s: it contains an open set containing s.

theorem exists_open_set_nhds' {α : Type u} [TopologicalSpace α] {s : Set α} {U : Set α} (h : U ∈ ⨆ (x : α) (_ : x ∈ s), nhds x) : ∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U

If U is a neighborhood of each point of a set s then it is a neighborhood of s: it contains an open set containing s.

theorem Filter.Eventually.eventually_nhds {α : Type u} [TopologicalSpace α] {p : α → Prop} {a : α} (h : ∀ᶠ (y : α) in nhds a, p y) : ∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhds y, p x

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

@[simp]

theorem eventually_eventually_nhds {α : Type u} [TopologicalSpace α] {p : α → Prop} {a : α} : (∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhds y, p x) ↔ ∀ᶠ (x : α) in nhds a, p x

@[simp]

theorem frequently_frequently_nhds {α : Type u} [TopologicalSpace α] {p : α → Prop} {a : α} : (∃ᶠ (y : α) in nhds a, ∃ᶠ (x : α) in nhds y, p x) ↔ ∃ᶠ (x : α) in nhds a, p x

@[simp]

theorem eventually_mem_nhds {α : Type u} [TopologicalSpace α] {s : Set α} {a : α} : (∀ᶠ (x : α) in nhds a, s ∈ nhds x) ↔ s ∈ nhds a

@[simp]

theorem nhds_bind_nhds {α : Type u} {a : α} [TopologicalSpace α] : Filter.bind (nhds a) nhds = nhds a

@[simp]

theorem eventually_eventuallyEq_nhds {α : Type u} {β : Type v} [TopologicalSpace α] {f : α → β} {g : α → β} {a : α} : (∀ᶠ (y : α) in nhds a, f =ᶠ[nhds y] g) ↔ f =ᶠ[nhds a] g

theorem Filter.EventuallyEq.eq_of_nhds {α : Type u} {β : Type v} [TopologicalSpace α] {f : α → β} {g : α → β} {a : α} (h : f =ᶠ[nhds a] g) : f a = g a

@[simp]

theorem eventually_eventuallyLE_nhds {α : Type u} {β : Type v} [TopologicalSpace α] [LE β] {f : α → β} {g : α → β} {a : α} : (∀ᶠ (y : α) in nhds a, f ≤ᶠ[nhds y] g) ↔ f ≤ᶠ[nhds a] g

theorem Filter.EventuallyEq.eventuallyEq_nhds {α : Type u} {β : Type v} [TopologicalSpace α] {f : α → β} {g : α → β} {a : α} (h : f =ᶠ[nhds a] g) : ∀ᶠ (y : α) in nhds a, f =ᶠ[nhds y] g

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

theorem Filter.EventuallyLE.eventuallyLE_nhds {α : Type u} {β : Type v} [TopologicalSpace α] [LE β] {f : α → β} {g : α → β} {a : α} (h : f ≤ᶠ[nhds a] g) : ∀ᶠ (y : α) in nhds a, f ≤ᶠ[nhds y] g

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

theorem all_mem_nhds {α : Type u} [TopologicalSpace α] (x : α) (P : Set α → Prop) (hP : (s t : Set α) → s ⊆ t → P s → P t) : ((s : Set α) → s ∈ nhds x → P s) ↔ (s : Set α) → IsOpen s → x ∈ s → P s

theorem all_mem_nhds_filter {α : Type u} {β : Type v} [TopologicalSpace α] (x : α) (f : Set α → Set β) (hf : ∀ (s t : Set α), s ⊆ t → f s ⊆ f t) (l : Filter β) : (∀ (s : Set α), s ∈ nhds x → f s ∈ l) ↔ ∀ (s : Set α), IsOpen s → x ∈ s → f s ∈ l

theorem tendsto_nhds {α : Type u} {β : Type v} [TopologicalSpace α] {f : β → α} {l : Filter β} {a : α} : Filter.Tendsto f l (nhds a) ↔ ∀ (s : Set α), IsOpen s → a ∈ s → f ⁻¹' s ∈ l

theorem tendsto_atTop_nhds {α : Type u} {β : Type v} [TopologicalSpace α] [Nonempty β] [SemilatticeSup β] {f : β → α} {a : α} : Filter.Tendsto f Filter.atTop (nhds a) ↔ ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : β), N ≤ n → f n ∈ U

theorem tendsto_const_nhds {α : Type u} {β : Type v} [TopologicalSpace α] {a : α} {f : Filter β} : Filter.Tendsto (fun x => a) f (nhds a)

theorem tendsto_atTop_of_eventually_const {α : Type u} [TopologicalSpace α] {ι : Type u_1} [SemilatticeSup ι] [Nonempty ι] {x : α} {u : ι → α} {i₀ : ι} (h : ∀ (i : ι), i ≥ i₀ → u i = x) : Filter.Tendsto u Filter.atTop (nhds x)

theorem tendsto_atBot_of_eventually_const {α : Type u} [TopologicalSpace α] {ι : Type u_1} [SemilatticeInf ι] [Nonempty ι] {x : α} {u : ι → α} {i₀ : ι} (h : ∀ (i : ι), i ≤ i₀ → u i = x) : Filter.Tendsto u Filter.atBot (nhds x)

theorem pure_le_nhds {α : Type u} [TopologicalSpace α] : pure ≤ nhds

theorem tendsto_pure_nhds {β : Type v} {α : Type u_1} [TopologicalSpace β] (f : α → β) (a : α) : Filter.Tendsto f (pure a) (nhds (f a))

theorem OrderTop.tendsto_atTop_nhds {β : Type v} {α : Type u_1} [PartialOrder α] [OrderTop α] [TopologicalSpace β] (f : α → β) : Filter.Tendsto f Filter.atTop (nhds (f ⊤))

@[simp]

instance nhds_neBot {α : Type u} [TopologicalSpace α] {a : α} : Filter.NeBot (nhds a)

Equations

• @nhds_neBot = @nhds_neBot.proof_1

theorem tendsto_nhds_of_eventually_eq {α : Type u} {β : Type v} [TopologicalSpace α] {l : Filter β} {f : β → α} {a : α} (h : ∀ᶠ (x : β) in l, f x = a) : Filter.Tendsto f l (nhds a)

Cluster points

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

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

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

Equations

• ClusterPt x F = Filter.NeBot (nhds x ⊓ F)

theorem ClusterPt.neBot {α : Type u} [TopologicalSpace α] {x : α} {F : Filter α} (h : ClusterPt x F) : Filter.NeBot (nhds x ⊓ F)

theorem Filter.HasBasis.clusterPt_iff {α : Type u} {a : α} [TopologicalSpace α] {ιa : Sort u_1} {ιF : Sort u_2} {pa : ιa → Prop} {sa : ιa → Set α} {pF : ιF → Prop} {sF : ιF → Set α} {F : Filter α} (ha : Filter.HasBasis (nhds a) pa sa) (hF : Filter.HasBasis F pF sF) : ClusterPt a F ↔ ∀ ⦃i : ιa⦄, pa i → ∀ ⦃j : ιF⦄, pF j → Set.Nonempty (sa i ∩ sF j)

theorem clusterPt_iff {α : Type u} [TopologicalSpace α] {x : α} {F : Filter α} : ClusterPt x F ↔ ∀ ⦃U : Set α⦄, U ∈ nhds x → ∀ ⦃V : Set α⦄, V ∈ F → Set.Nonempty (U ∩ V)

theorem clusterPt_iff_not_disjoint {α : Type u} [TopologicalSpace α] {x : α} {F : Filter α} : ClusterPt x F ↔ ¬Disjoint (nhds x) F

theorem clusterPt_principal_iff {α : Type u} [TopologicalSpace α] {x : α} {s : Set α} : ClusterPt x (Filter.principal s) ↔ ∀ (U : Set α), 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 {α : Type u} [TopologicalSpace α] {x : α} {s : Set α} : ClusterPt x (Filter.principal s) ↔ ∃ᶠ (y : α) in nhds x, y ∈ s

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

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

theorem ClusterPt.of_nhds_le {α : Type u} [TopologicalSpace α] {x : α} {f : Filter α} (H : nhds x ≤ f) : ClusterPt x f

theorem ClusterPt.mono {α : Type u} [TopologicalSpace α] {x : α} {f : Filter α} {g : Filter α} (H : ClusterPt x f) (h : f ≤ g) : ClusterPt x g

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

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

theorem Ultrafilter.clusterPt_iff {α : Type u} [TopologicalSpace α] {x : α} {f : Ultrafilter α} : ClusterPt x ↑f ↔ ↑f ≤ nhds x

def MapClusterPt {α : Type u} [TopologicalSpace α] {ι : Type u_1} (x : α) (F : Filter ι) (u : ι → α) : Prop

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

Equations

• MapClusterPt x F u = ClusterPt x (Filter.map u F)

theorem mapClusterPt_iff {α : Type u} [TopologicalSpace α] {ι : Type u_1} (x : α) (F : Filter ι) (u : ι → α) : MapClusterPt x F u ↔ ∀ (s : Set α), s ∈ nhds x → ∃ᶠ (a : ι) in F, u a ∈ s

theorem mapClusterPt_of_comp {α : Type u} [TopologicalSpace α] {ι : Type u_1} {δ : Type u_2} {F : Filter ι} {φ : δ → ι} {p : Filter δ} {x : α} {u : ι → α} [Filter.NeBot p] (h : Filter.Tendsto φ p F) (H : Filter.Tendsto (u ∘ φ) p (nhds x)) : MapClusterPt x F u

def AccPt {α : Type u} [TopologicalSpace α] (x : α) (F : Filter α) : Prop

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

Equations

• AccPt x F = Filter.NeBot (nhdsWithin x {x}ᶜ ⊓ F)

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

theorem acc_principal_iff_cluster {α : Type u} [TopologicalSpace α] (x : α) (C : Set α) : 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 {α : Type u} [TopologicalSpace α] (x : α) (C : Set α) : AccPt x (Filter.principal C) ↔ ∀ (U : Set α), U ∈ nhds x → ∃ y, y ∈ U ∩ C ∧ y ≠ x

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

theorem accPt_iff_frequently {α : Type u} [TopologicalSpace α] (x : α) (C : Set α) : AccPt x (Filter.principal C) ↔ ∃ᶠ (y : α) 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 {α : Type u} [TopologicalSpace α] {x : α} {F : Filter α} {G : Filter α} (h : AccPt x F) (hFG : F ≤ G) : AccPt x G

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

Interior, closure and frontier in terms of neighborhoods

theorem interior_eq_nhds' {α : Type u} [TopologicalSpace α] {s : Set α} : interior s = {a | s ∈ nhds a}

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

@[simp]

theorem interior_mem_nhds {α : Type u} [TopologicalSpace α] {s : Set α} {a : α} : interior s ∈ nhds a ↔ s ∈ nhds a

theorem interior_setOf_eq {α : Type u} [TopologicalSpace α] {p : α → Prop} : interior {x | p x} = {x | ∀ᶠ (y : α) in nhds x, p y}

theorem isOpen_setOf_eventually_nhds {α : Type u} [TopologicalSpace α] {p : α → Prop} : IsOpen {x | ∀ᶠ (y : α) in nhds x, p y}

theorem subset_interior_iff_nhds {α : Type u} [TopologicalSpace α] {s : Set α} {V : Set α} : s ⊆ interior V ↔ ∀ (x : α), x ∈ s → V ∈ nhds x

theorem isOpen_iff_nhds {α : Type u} [TopologicalSpace α] {s : Set α} : IsOpen s ↔ ∀ (a : α), a ∈ s → nhds a ≤ Filter.principal s

theorem isOpen_iff_mem_nhds {α : Type u} [TopologicalSpace α] {s : Set α} : IsOpen s ↔ ∀ (a : α), a ∈ s → s ∈ nhds a

theorem isOpen_iff_eventually {α : Type u} [TopologicalSpace α] {s : Set α} : IsOpen s ↔ ∀ (x : α), x ∈ s → ∀ᶠ (y : α) 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 {α : Type u} [TopologicalSpace α] {s : Set α} : IsOpen s ↔ ∀ (x : α), x ∈ s → ∀ (l : Ultrafilter α), ↑l ≤ nhds x → s ∈ l

theorem isOpen_singleton_iff_nhds_eq_pure {α : Type u} [TopologicalSpace α] (a : α) : IsOpen {a} ↔ nhds a = pure a

theorem isOpen_singleton_iff_punctured_nhds {α : Type u_1} [TopologicalSpace α] (a : α) : IsOpen {a} ↔ nhdsWithin a {a}ᶜ = ⊥

theorem mem_closure_iff_frequently {α : Type u} [TopologicalSpace α] {s : Set α} {a : α} : a ∈ closure s ↔ ∃ᶠ (x : α) in nhds a, x ∈ s

theorem Filter.Frequently.mem_closure {α : Type u} [TopologicalSpace α] {s : Set α} {a : α} : (∃ᶠ (x : α) in nhds a, x ∈ s) → a ∈ closure s

Alias of the reverse direction of mem_closure_iff_frequently.

theorem isClosed_iff_frequently {α : Type u} [TopologicalSpace α] {s : Set α} : IsClosed s ↔ ∀ (x : α), (∃ᶠ (y : α) 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 {α : Type u} [TopologicalSpace α] {f : Filter α} : IsClosed {x | ClusterPt x f}

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

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

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

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

theorem dense_compl_singleton {α : Type u} [TopologicalSpace α] (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 {α : Type u} [TopologicalSpace α] (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 {α : Type u} [TopologicalSpace α] (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 {α : Type u} [TopologicalSpace α] (x : α) [Filter.NeBot (nhdsWithin x {x}ᶜ)] : ¬IsOpen {x}

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

theorem mem_closure_iff_nhds {α : Type u} [TopologicalSpace α] {s : Set α} {a : α} : a ∈ closure s ↔ ∀ (t : Set α), t ∈ nhds a → Set.Nonempty (t ∩ s)

theorem mem_closure_iff_nhds' {α : Type u} [TopologicalSpace α] {s : Set α} {a : α} : a ∈ closure s ↔ ∀ (t : Set α), t ∈ nhds a → ∃ y, ↑y ∈ t

theorem mem_closure_iff_comap_neBot {α : Type u} [TopologicalSpace α] {A : Set α} {x : α} : x ∈ closure A ↔ Filter.NeBot (Filter.comap Subtype.val (nhds x))

theorem mem_closure_iff_nhds_basis' {α : Type u} {ι : Sort w} [TopologicalSpace α] {a : α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis (nhds a) p s) {t : Set α} : a ∈ closure t ↔ ∀ (i : ι), p i → Set.Nonempty (s i ∩ t)

theorem mem_closure_iff_nhds_basis {α : Type u} {ι : Sort w} [TopologicalSpace α] {a : α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis (nhds a) p s) {t : Set α} : a ∈ closure t ↔ ∀ (i : ι), p i → ∃ y, y ∈ t ∧ y ∈ s i

theorem clusterPt_iff_forall_mem_closure {α : Type u} [TopologicalSpace α] {F : Filter α} {a : α} : ClusterPt a F ↔ ∀ (s : Set α), s ∈ F → a ∈ closure s

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

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

@[simp]

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

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

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

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

theorem isClosed_iff_nhds {α : Type u} [TopologicalSpace α] {s : Set α} : IsClosed s ↔ ∀ (x : α), (∀ (U : Set α), U ∈ nhds x → Set.Nonempty (U ∩ s)) → x ∈ s

theorem IsClosed.interior_union_left {α : Type u} [TopologicalSpace α] {s : Set α} {t : Set α} : IsClosed s → interior (s ∪ t) ⊆ s ∪ interior t

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

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

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

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

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

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

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

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

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

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

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

theorem Filter.Frequently.mem_of_closed {α : Type u} [TopologicalSpace α] {a : α} {s : Set α} (h : ∃ᶠ (x : α) in nhds a, x ∈ s) (hs : IsClosed s) : a ∈ s

theorem IsClosed.mem_of_frequently_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] {f : β → α} {b : Filter β} {a : α} {s : Set α} (hs : IsClosed s) (h : ∃ᶠ (x : β) in b, f x ∈ s) (hf : Filter.Tendsto f b (nhds a)) : a ∈ s

theorem IsClosed.mem_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] {f : β → α} {b : Filter β} {a : α} {s : Set α} [Filter.NeBot b] (hs : IsClosed s) (hf : Filter.Tendsto f b (nhds a)) (h : ∀ᶠ (x : β) in b, f x ∈ s) : a ∈ s

theorem mem_closure_of_frequently_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] {f : β → α} {b : Filter β} {a : α} {s : Set α} (h : ∃ᶠ (x : β) in b, f x ∈ s) (hf : Filter.Tendsto f b (nhds a)) : a ∈ closure s

theorem mem_closure_of_tendsto {α : Type u} {β : Type v} [TopologicalSpace α] {f : β → α} {b : Filter β} {a : α} {s : Set α} [Filter.NeBot b] (hf : Filter.Tendsto f b (nhds a)) (h : ∀ᶠ (x : β) in b, f x ∈ s) : a ∈ closure s

theorem tendsto_inf_principal_nhds_iff_of_forall_eq {α : Type u} {β : Type v} [TopologicalSpace α] {f : β → α} {l : Filter β} {s : Set β} {a : α} (h : ∀ (x : β), ¬x ∈ s → f x = a) : Filter.Tendsto f (l ⊓ Filter.principal s) (nhds a) ↔ Filter.Tendsto f l (nhds a)

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

Limits of filters in topological spaces

In this section we define functions that return a limit of a filter (or of a function along a filter), if it exists, and a random point otherwise. 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 = a is not equivalent to Filter.Tendsto g f (𝓝 a) unless the codomain is a Hausdorff space and g has a limit along f.

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

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

Equations

• lim f = Classical.epsilon fun a => f ≤ nhds a

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

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

Equations

• Ultrafilter.lim F = lim ↑F

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

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

Equations

• limUnder f g = lim (Filter.map g f)

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

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

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

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

Continuity

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

• isOpen_preimage : ∀ (s : Set β), IsOpen s → IsOpen (f ⁻¹' s)

  The preimage of an open set under a continuous function is an open set. Use IsOpen.preimage instead.

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

def Topology.Continuous_of : Lean.ParserDescr

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

Equations

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

theorem continuous_def {α : Type u_1} {β : Type u_2} : ∀ {x : TopologicalSpace α} {x_1 : TopologicalSpace β} {f : α → β}, Continuous f ↔ ∀ (s : Set β), IsOpen s → IsOpen (f ⁻¹' s)

theorem IsOpen.preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) {s : Set β} (h : IsOpen s) : IsOpen (f ⁻¹' s)

theorem Continuous.congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} (h : Continuous f) (h' : ∀ (x : α), f x = g x) : Continuous g

def ContinuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (x : α) : Prop

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

Equations

• ContinuousAt f x = Filter.Tendsto f (nhds x) (nhds (f x))

theorem ContinuousAt.tendsto {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} (h : ContinuousAt f x) : Filter.Tendsto f (nhds x) (nhds (f x))

theorem continuousAt_def {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} : ContinuousAt f x ↔ ∀ (A : Set β), A ∈ nhds (f x) → f ⁻¹' A ∈ nhds x

theorem continuousAt_congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} {x : α} (h : f =ᶠ[nhds x] g) : ContinuousAt f x ↔ ContinuousAt g x

theorem ContinuousAt.congr {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {g : α → β} {x : α} (hf : ContinuousAt f x) (h : f =ᶠ[nhds x] g) : ContinuousAt g x

theorem ContinuousAt.preimage_mem_nhds {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {t : Set β} (h : ContinuousAt f x) (ht : t ∈ nhds (f x)) : f ⁻¹' t ∈ nhds x

theorem eventuallyEq_zero_nhds {α : Type u_1} [TopologicalSpace α] {M₀ : Type u_5} [Zero M₀] {a : α} {f : α → M₀} : f =ᶠ[nhds a] 0 ↔ ¬a ∈ closure (Function.support f)

theorem ClusterPt.map {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {la : Filter α} {lb : Filter β} (H : ClusterPt x la) {f : α → β} (hfc : ContinuousAt f x) (hf : Filter.Tendsto f la lb) : ClusterPt (f x) lb

theorem preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set β} (hf : Continuous f) : f ⁻¹' interior s ⊆ interior (f ⁻¹' s)

See also interior_preimage_subset_preimage_interior.

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

theorem continuous_id' {α : Type u_1} [TopologicalSpace α] : Continuous fun x => x

theorem Continuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) : Continuous (g ∘ f)

theorem Continuous.comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} (hg : Continuous g) (hf : Continuous f) : Continuous fun x => g (f x)

theorem Continuous.iterate {α : Type u_1} [TopologicalSpace α] {f : α → α} (h : Continuous f) (n : ℕ) : Continuous f^[n]

theorem ContinuousAt.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {x : α} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) : ContinuousAt (g ∘ f) x

theorem ContinuousAt.comp_of_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] {g : β → γ} {f : α → β} {x : α} {y : β} (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 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) (x : α) : Filter.Tendsto f (nhds x) (nhds (f x))

theorem Continuous.tendsto' {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) (x : α) (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 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} (h : Continuous f) : ContinuousAt f x

theorem continuous_iff_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : Continuous f ↔ ∀ (x : α), ContinuousAt f x

theorem continuousAt_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {b : β} : ContinuousAt (fun x => b) x

theorem continuous_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {b : β} : Continuous fun x => b

theorem Filter.EventuallyEq.continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {x : α} {f : α → β} {y : β} (h : f =ᶠ[nhds x] fun x => y) : ContinuousAt f x

theorem continuous_of_const {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (h : ∀ (x y : α), f x = f y) : Continuous f

theorem continuousAt_id {α : Type u_1} [TopologicalSpace α] {x : α} : ContinuousAt id x

theorem ContinuousAt.iterate {α : Type u_1} [TopologicalSpace α] {f : α → α} {x : α} (hf : ContinuousAt f x) (hx : f x = x) (n : ℕ) : ContinuousAt f^[n] x

theorem continuous_iff_isClosed {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : Continuous f ↔ ∀ (s : Set β), IsClosed s → IsClosed (f ⁻¹' s)

theorem IsClosed.preimage {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) {s : Set β} (h : IsClosed s) : IsClosed (f ⁻¹' s)

theorem mem_closure_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} {s : Set α} (hf : ContinuousAt f x) (hx : x ∈ closure s) : f x ∈ closure (f '' s)

theorem continuousAt_iff_ultrafilter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {x : α} : ContinuousAt f x ↔ ∀ (g : Ultrafilter α), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))

theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} : Continuous f ↔ ∀ (x : α) (g : Ultrafilter α), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))

theorem Continuous.closure_preimage_subset {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) (t : Set β) : closure (f ⁻¹' t) ⊆ f ⁻¹' closure t

theorem Continuous.frontier_preimage_subset {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) (t : Set β) : frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t

theorem Set.MapsTo.closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} {f : α → β} (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 {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) : f '' closure s ⊆ closure (f '' s)

See also IsClosedMap.closure_image_eq_of_continuous.

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

theorem closure_subset_preimage_closure_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) : closure s ⊆ f ⁻¹' closure (f '' s)

theorem map_mem_closure {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} {f : α → β} {a : α} (hf : Continuous f) (ha : a ∈ closure s) (ht : Set.MapsTo f s t) : f a ∈ closure t

theorem Set.MapsTo.closure_left {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {s : Set α} {t : Set β} {f : α → β} (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.

Function with dense range

def DenseRange {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} (f : κ → β) : Prop

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

Equations

• DenseRange f = Dense (Set.range f)

theorem Function.Surjective.denseRange {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} (hf : Function.Surjective f) : DenseRange f

A surjective map has dense range.

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

theorem denseRange_iff_closure_range {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} : DenseRange f ↔ closure (Set.range f) = Set.univ

theorem DenseRange.closure_range {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} (h : DenseRange f) : closure (Set.range f) = Set.univ

theorem Dense.denseRange_val {α : Type u_1} [TopologicalSpace α] {s : Set α} (h : Dense s) : DenseRange Subtype.val

theorem Continuous.range_subset_closure_image_dense {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf : Continuous f) {s : Set α} (hs : Dense s) : Set.range f ⊆ closure (f '' s)

theorem DenseRange.dense_image {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf' : DenseRange f) (hf : Continuous f) {s : Set α} (hs : Dense s) : Dense (f '' s)

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

theorem DenseRange.subset_closure_image_preimage_of_isOpen {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} (hf : DenseRange f) {s : Set β} (hs : IsOpen s) : s ⊆ closure (f '' (f ⁻¹' s))

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

theorem DenseRange.dense_of_mapsTo {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [TopologicalSpace β] {f : α → β} (hf' : DenseRange f) (hf : Continuous f) {s : Set α} (hs : Dense s) {t : Set β} (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 {β : Type u_2} {γ : Type u_3} [TopologicalSpace β] [TopologicalSpace γ] {κ : Type u_5} {g : β → γ} {f : κ → β} (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 {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} (hf : DenseRange f) : Nonempty κ ↔ Nonempty β

theorem DenseRange.nonempty {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} [h : Nonempty β] (hf : DenseRange f) : Nonempty κ

def DenseRange.some {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} (hf : DenseRange f) (b : β) : κ

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

Equations

• DenseRange.some hf b = Classical.choice (_ : Nonempty κ)

theorem DenseRange.exists_mem_open {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} (hf : DenseRange f) {s : Set β} (ho : IsOpen s) (hs : Set.Nonempty s) : ∃ a, f a ∈ s

theorem DenseRange.mem_nhds {β : Type u_2} [TopologicalSpace β] {κ : Type u_5} {f : κ → β} (h : DenseRange f) {b : β} {U : Set β} (U_in : U ∈ nhds b) : ∃ a, f a ∈ U