Documentation

Mathlib.Topology.Basic

Basic theory of topological spaces. #

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

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

Notation #

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

𝓝 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

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

Instances For

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

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

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

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

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

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

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

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

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

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

(_ : Filter.NeBot (nhds x)) = (_ : Filter.NeBot (nhds x))

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

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

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

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

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

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

theorem Ultrafilter.clusterPt_iff {X : Type u} {x : X} [TopologicalSpace X] {f : Ultrafilter X} :

ClusterPt x ↑f ↔ ↑f ≤ nhds x

theorem clusterPt_iff_ultrafilter {X : Type u} {x : X} [TopologicalSpace X] {f : Filter X} :

ClusterPt x f ↔ ∃ (u : Ultrafilter X), ↑u ≤ f ∧ ↑u ≤ nhds x

theorem mapClusterPt_def {X : Type u} [TopologicalSpace X] {ι : Type u_3} (x : X) (F : Filter ι) (u : ι → X) :

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

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 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}ᶜ)] :

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}ᶜ)] :

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} [TopologicalSpace X] [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) :

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

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

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

theorem continuousAt_id {X : Type u_1} [TopologicalSpace X] {x : X} :

ContinuousAt id x

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.

Function with dense range #

theorem Function.Surjective.denseRange {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} (hf : Function.Surjective f) :

A surjective map has dense range.

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

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

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

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 (_ : Nonempty α)

Instances For

theorem DenseRange.exists_mem_open {X : Type u_1} [TopologicalSpace X] {α : Type u_4} {f : α → X} {s : Set X} (hf : DenseRange f) (ho : IsOpen s) (hs : Set.Nonempty s) :

∃ (a : α), f a ∈ s

theorem DenseRange.mem_nhds {X : Type u_1} [TopologicalSpace X] {x : X} {α : Type u_4} {f : α → X} {s : Set X} (h : DenseRange f) (hs : s ∈ nhds x) :

∃ (a : α), f a ∈ s