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 https://leanprover-community.github.io/theories/topology.html.

References #

Tags #

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

Topological spaces #

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

TopologicalSpace X

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

Equations

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

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 : s.Finite) :

(∀ 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 : s.Finite) (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 : s.Finite) (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 : s.Finite) (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 : S.Finite) :

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)

@[simp]

theorem interior_iInter₂_lt_nat {X : Type u} [TopologicalSpace X] {n : ℕ} (f : ℕ → Set X) :

interior (⋂ (m : ℕ), ⋂ (_ : m < n), f m) = ⋂ (m : ℕ), ⋂ (_ : m < n), interior (f m)

@[simp]

theorem interior_iInter₂_le_nat {X : Type u} [TopologicalSpace X] {n : ℕ} (f : ℕ → Set X) :

interior (⋂ (m : ℕ), ⋂ (_ : m ≤ n), f m) = ⋂ (m : ℕ), ⋂ (_ : m ≤ n), interior (f m)

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 : l.HasBasis p s) :

(l.lift' interior).HasBasis p fun (i : ι) => interior (s i)

theorem Filter.lift'_interior_le {X : Type u} [TopologicalSpace X] (l : Filter X) :

l.lift' 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 : l.HasBasis p s) (ho : ∀ (i : ι), p i → IsOpen (s i)) :

l.lift' 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] :

(closure s).Nonempty ↔ s.Nonempty

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

(closure s).Nonempty → s.Nonempty

Alias of the forward direction of closure_nonempty_iff.

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

s.Nonempty → (closure s).Nonempty

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 : s.Finite) (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 : S.Finite) :

closure (⋃₀ S) = ⋃ s ∈ S, closure s

@[simp]

theorem Finset.closure_biUnion {X : Type u} [TopologicalSpace X] {ι : Type u_3} (s : Finset ι) (f : ι → Set X) :

closure (⋃ i ∈ s, f i) = ⋃ i ∈ s, closure (f i)

@[simp]

theorem closure_iUnion_of_finite {X : Type u} {ι : Sort w} [TopologicalSpace X] [Finite ι] (f : ι → Set X) :

closure (⋃ (i : ι), f i) = ⋃ (i : ι), closure (f i)

@[simp]

theorem closure_iUnion₂_lt_nat {X : Type u} [TopologicalSpace X] {n : ℕ} (f : ℕ → Set X) :

closure (⋃ (m : ℕ), ⋃ (_ : m < n), f m) = ⋃ (m : ℕ), ⋃ (_ : m < n), closure (f m)

@[simp]

theorem closure_iUnion₂_le_nat {X : Type u} [TopologicalSpace X] {n : ℕ} (f : ℕ → Set X) :

closure (⋃ (m : ℕ), ⋃ (_ : m ≤ n), f m) = ⋃ (m : ℕ), ⋃ (_ : m ≤ n), closure (f m)

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 → (o ∩ s).Nonempty

theorem closure_inter_open_nonempty_iff {X : Type u} {s : Set X} {t : Set X} [TopologicalSpace X] (h : IsOpen t) :

(closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty

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

l ≤ l.lift' closure

theorem Filter.HasBasis.lift'_closure {X : Type u} {ι : Sort w} [TopologicalSpace X] {l : Filter X} {p : ι → Prop} {s : ι → Set X} (h : l.HasBasis p s) :

(l.lift' closure).HasBasis 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 : l.HasBasis p s) (hc : ∀ (i : ι), p i → IsClosed (s i)) :

l.lift' closure = l

@[simp]

theorem Filter.lift'_closure_eq_bot {X : Type u} [TopologicalSpace X] {l : Filter X} :

l.lift' 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 → U.Nonempty → (U ∩ s).Nonempty

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 → U.Nonempty → (U ∩ s).Nonempty

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 : U.Nonempty) :

∃ x ∈ s, x ∈ U

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

s.Nonempty ↔ Nonempty X

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

s.Nonempty

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.

theorem IsOpen.subset_interior_closure {X : Type u} [TopologicalSpace X] {s : Set X} (s_open : IsOpen s) :

s ⊆ interior (closure s)

theorem IsClosed.closure_interior_subset {X : Type u} [TopologicalSpace X] {s : Set X} (s_closed : IsClosed s) :

closure (interior s) ⊆ s

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 frontier_subset_iff_isClosed {X : Type u} {s : Set X} [TopologicalSpace X] :

frontier s ⊆ s ↔ IsClosed s

theorem IsClosed.frontier_subset {X : Type u} {s : Set X} [TopologicalSpace X] :

IsClosed s → frontier s ⊆ s

Alias of the reverse direction of frontier_subset_iff_isClosed.

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 disjoint_frontier_iff_isOpen {X : Type u} {s : Set X} [TopologicalSpace X] :

Disjoint (frontier s) s ↔ IsOpen 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) :

(nhds x).HasBasis (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) :

(nhds x).HasBasis (fun (s : Set X) => x ∉ s ∧ IsClosed s) compl

@[simp]

theorem lift'_nhds_interior {X : Type u} [TopologicalSpace X] (x : X) :

(nhds x).lift' interior = nhds x

theorem Filter.HasBasis.nhds_interior {X : Type u} {ι : Sort w} [TopologicalSpace X] {x : X} {p : ι → Prop} {s : ι → Set X} (h : (nhds x).HasBasis p s) :

(nhds x).HasBasis 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} :

(∀ᶠ (y : X) in nhds x, p y) ↔ ∃ (t : Set X), (∀ y ∈ t, p y) ∧ 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 frequently_nhds_iff {X : Type u} {x : X} [TopologicalSpace X] {p : X → Prop} :

(∃ᶠ (y : X) in nhds x, p y) ↔ ∀ (U : Set X), x ∈ U → IsOpen U → ∃ y ∈ U, p y

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

(nhds x).HasBasis (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] :

(nhds x).bind 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] :

(nhds x).NeBot

Equations

⋯ = ⋯

theorem tendsto_nhds_of_eventually_eq {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {l : Filter α} {f : α → X} (h : ∀ᶠ (x' : α) in l, f x' = x) :

Filter.Tendsto f l (nhds x)

theorem Filter.EventuallyEq.tendsto {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {l : Filter α} {f : α → X} (hf : f =ᶠ[l] fun (x_1 : α) => x) :

Filter.Tendsto f l (nhds x)

Cluster points #

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

theorem ClusterPt.neBot {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} (h : ClusterPt x F) :

(nhds x ⊓ F).NeBot

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 : (nhds x).HasBasis pX sX) (hF : F.HasBasis pF sF) :

ClusterPt x F ↔ ∀ ⦃i : ιX⦄, pX i → ∀ ⦃j : ιF⦄, pF j → (sX i ∩ sF j).Nonempty

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 → (U ∩ V).Nonempty

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, (U ∩ s).Nonempty

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) [f.NeBot] :

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

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

MapClusterPt x F (u ∘ φ) ↔ MapClusterPt x (Filter.map φ F) u

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

MapClusterPt x F u

theorem accPt_sup {X : Type u} [TopologicalSpace X] (x : X) (F : Filter X) (G : Filter X) :

AccPt x (F ⊔ G) ↔ AccPt x F ∨ AccPt x G

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 G.

theorem AccPt.clusterPt {X : Type u} [TopologicalSpace X] (x : X) (F : Filter X) (h : AccPt x F) :

Interior, closure and frontier in terms of neighborhoods #

theorem interior_eq_nhds' {X : Type u} {s : Set X} [TopologicalSpace X] :

interior s = {x : X | s ∈ nhds x}

theorem interior_eq_nhds {X : Type u} {s : Set X} [TopologicalSpace X] :

interior s = {x : X | nhds x ≤ Filter.principal s}

@[simp]

theorem interior_mem_nhds {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :

interior s ∈ nhds x ↔ s ∈ nhds x

theorem interior_setOf_eq {X : Type u} [TopologicalSpace X] {p : X → Prop} :

interior {x : X | p x} = {x : X | ∀ᶠ (y : X) in nhds x, p y}

theorem isOpen_setOf_eventually_nhds {X : Type u} [TopologicalSpace X] {p : X → Prop} :

IsOpen {x : X | ∀ᶠ (y : X) in nhds x, p y}

theorem subset_interior_iff_nhds {X : Type u} {s : Set X} [TopologicalSpace X] {V : Set X} :

s ⊆ interior V ↔ ∀ x ∈ s, V ∈ nhds x

theorem isOpen_iff_nhds {X : Type u} {s : Set X} [TopologicalSpace X] :

IsOpen s ↔ ∀ x ∈ s, nhds x ≤ Filter.principal s

theorem TopologicalSpace.ext_iff_nhds {X : Type u} {t : TopologicalSpace X} {t' : TopologicalSpace X} :

t = t' ↔ ∀ (x : X), nhds x = nhds x

theorem TopologicalSpace.ext_nhds {X : Type u} {t : TopologicalSpace X} {t' : TopologicalSpace X} :

(∀ (x : X), nhds x = nhds x) → t = t'

Alias of the reverse direction of TopologicalSpace.ext_iff_nhds.

theorem isOpen_iff_mem_nhds {X : Type u} {s : Set X} [TopologicalSpace X] :

IsOpen s ↔ ∀ x ∈ s, s ∈ nhds x

theorem isOpen_iff_eventually {X : Type u} {s : Set X} [TopologicalSpace X] :

IsOpen s ↔ ∀ x ∈ s, ∀ᶠ (y : X) in nhds x, y ∈ s

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

theorem isOpen_iff_ultrafilter {X : Type u} {s : Set X} [TopologicalSpace X] :

IsOpen s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), ↑l ≤ nhds x → s ∈ l

theorem isOpen_singleton_iff_nhds_eq_pure {X : Type u} [TopologicalSpace X] (x : X) :

IsOpen {x} ↔ nhds x = pure x

theorem isOpen_singleton_iff_punctured_nhds {X : Type u} [TopologicalSpace X] (x : X) :

IsOpen {x} ↔ nhdsWithin x {x}ᶜ = ⊥

theorem mem_closure_iff_frequently {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :

x ∈ closure s ↔ ∃ᶠ (x : X) in nhds x, x ∈ s

theorem Filter.Frequently.mem_closure {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :

(∃ᶠ (x : X) in nhds x, x ∈ s) → x ∈ closure s

Alias of the reverse direction of mem_closure_iff_frequently.

theorem isClosed_iff_frequently {X : Type u} {s : Set X} [TopologicalSpace X] :

IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in nhds x, y ∈ s) → x ∈ s

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

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

IsClosed {x : X | ClusterPt x f}

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

theorem mem_closure_iff_clusterPt {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :

x ∈ closure s ↔ ClusterPt x (Filter.principal s)

theorem mem_closure_iff_nhds_ne_bot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :

x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥

@[deprecated mem_closure_iff_nhds_ne_bot]

theorem mem_closure_iff_nhds_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :

x ∈ closure s ↔ nhds x ⊓ Filter.principal s ≠ ⊥

Alias of mem_closure_iff_nhds_ne_bot.

theorem mem_closure_iff_nhdsWithin_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :

x ∈ closure s ↔ (nhdsWithin x s).NeBot

theorem nhdsWithin_neBot {X : Type u} {x : X} {s : Set X} [TopologicalSpace X] :

(nhdsWithin x s).NeBot ↔ ∀ ⦃t : Set X⦄, t ∈ nhds x → (t ∩ s).Nonempty

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

nhdsWithin x s ≤ nhdsWithin x t

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) [(nhdsWithin x {x}ᶜ).NeBot] :

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) [(nhdsWithin x {x}ᶜ).NeBot] :

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) [(nhdsWithin x {x}ᶜ).NeBot] :

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) [(nhdsWithin x {x}ᶜ).NeBot] :

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, (t ∩ s).Nonempty

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.comap Subtype.val (nhds x)).NeBot

theorem mem_closure_iff_nhds_basis' {X : Type u} {ι : Sort w} {x : X} {t : Set X} [TopologicalSpace X] {p : ι → Prop} {s : ι → Set X} (h : (nhds x).HasBasis p s) :

x ∈ closure t ↔ ∀ (i : ι), p i → (s i ∩ t).Nonempty

theorem mem_closure_iff_nhds_basis {X : Type u} {ι : Sort w} {x : X} {t : Set X} [TopologicalSpace X] {p : ι → Prop} {s : ι → Set X} (h : (nhds x).HasBasis 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 ≤ F.lift' closure

theorem clusterPt_iff_lift'_closure' {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :

ClusterPt x F ↔ (F.lift' closure ⊓ pure x).NeBot

@[simp]

theorem clusterPt_lift'_closure_iff {X : Type u} {x : X} [TopologicalSpace X] {F : Filter X} :

ClusterPt x (F.lift' 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, (U ∩ s).Nonempty) → x ∈ s

theorem isClosed_iff_forall_filter {X : Type u} {s : Set X} [TopologicalSpace X] :

IsClosed s ↔ ∀ (x : X) (F : Filter X), F.NeBot → 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) :

(s ∩ t).Nonempty

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 α} [b.NeBot] (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 α} [b.NeBot] (hf : Filter.Tendsto f b (nhds x)) (h : ∀ᶠ (x : α) in b, f x ∈ s) :

x ∈ closure s

theorem tendsto_inf_principal_nhds_iff_of_forall_eq {X : Type u} {α : Type u_1} {x : X} [TopologicalSpace X] {f : α → X} {l : Filter α} {s : Set α} (h : ∀ a ∉ s, f a = x) :

Filter.Tendsto f (l ⊓ Filter.principal s) (nhds x) ↔ Filter.Tendsto f l (nhds x)

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

Limits of filters in topological spaces #

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

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

f ≤ nhds (lim f)

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

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

Filter.Tendsto g f (nhds (limUnder f g))

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

Continuity #

theorem continuous_def {X : Type u_1} {Y : Type u_2} :

∀ {x : TopologicalSpace X} {x_1 : TopologicalSpace Y} {f : X → Y}, Continuous f ↔ ∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)

theorem IsOpen.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {t : Set Y} (h : IsOpen t) :

IsOpen (f ⁻¹' t)

theorem continuous_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {g : X → Y} (h : ∀ (x : X), f x = g x) :

Continuous f ↔ Continuous g

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

theorem ContinuousAt.tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (h : ContinuousAt f x) :

Filter.Tendsto f (nhds x) (nhds (f x))

theorem continuousAt_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} :

ContinuousAt f x ↔ ∀ A ∈ nhds (f x), f ⁻¹' A ∈ nhds x

theorem continuousAt_congr {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {g : X → Y} (h : f =ᶠ[nhds x] g) :

ContinuousAt f x ↔ ContinuousAt g x

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

ContinuousAt g x

theorem ContinuousAt.preimage_mem_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {t : Set Y} (h : ContinuousAt f x) (ht : t ∈ nhds (f x)) :

f ⁻¹' t ∈ nhds x

theorem ContinuousAt.eventually_mem {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (hf : ContinuousAt f x) {s : Set Y} (hs : s ∈ nhds (f x)) :

∀ᶠ (y : X) in nhds x, f y ∈ s

If f x ∈ s ∈ 𝓝 (f x) for continuous f, then f y ∈ s near x.

This is essentially Filter.Tendsto.eventually_mem, but infers in more cases when applied.

@[deprecated]

theorem eventuallyEq_zero_nhds {X : Type u_1} [TopologicalSpace X] {x : X} {M₀ : Type u_4} [Zero M₀] {f : X → M₀} :

f =ᶠ[nhds x] 0 ↔ x ∉ closure (Function.support f)

Deprecated, please use not_mem_tsupport_iff_eventuallyEq instead.

theorem ClusterPt.map {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} {lx : Filter X} {ly : Filter Y} (H : ClusterPt x lx) (hfc : ContinuousAt f x) (hf : Filter.Tendsto f lx ly) :

ClusterPt (f x) ly

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

f ⁻¹' interior t ⊆ interior (f ⁻¹' t)

See also interior_preimage_subset_preimage_interior.

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

theorem continuous_id' {X : Type u_1} [TopologicalSpace X] :

Continuous fun (x : X) => x

theorem Continuous.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : Continuous g) (hf : Continuous f) :

Continuous (g ∘ f)

theorem Continuous.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hg : Continuous g) (hf : Continuous f) :

Continuous fun (x : X) => g (f x)

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

Continuous f^[n]

theorem ContinuousAt.comp {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {x : X} {g : Y → Z} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) :

ContinuousAt (g ∘ f) x

theorem ContinuousAt.comp' {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} {x : X} (hg : ContinuousAt g (f x)) (hf : ContinuousAt f x) :

ContinuousAt (fun (x : X) => g (f x)) x

theorem ContinuousAt.comp_of_eq {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {x : X} {y : Y} {g : Y → Z} (hg : ContinuousAt g y) (hf : ContinuousAt f x) (hy : f x = y) :

ContinuousAt (g ∘ f) x

See note [comp_of_eq lemmas]

theorem Continuous.tendsto {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) :

Filter.Tendsto f (nhds x) (nhds (f x))

theorem Continuous.tendsto' {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) (y : Y) (h : f x = y) :

Filter.Tendsto f (nhds x) (nhds y)

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

theorem Continuous.continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} (h : Continuous f) :

ContinuousAt f x

theorem continuous_iff_continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

Continuous f ↔ ∀ (x : X), ContinuousAt f x

theorem continuousAt_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} :

ContinuousAt (fun (x : X) => y) x

theorem continuous_const {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {y : Y} :

Continuous fun (x : X) => y

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

ContinuousAt f x

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

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

ContinuousAt id x

theorem continuousAt_id' {X : Type u_1} [TopologicalSpace X] (y : X) :

ContinuousAt (fun (x : X) => x) y

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

ContinuousAt f^[n] x

theorem continuous_iff_isClosed {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

Continuous f ↔ ∀ (s : Set Y), IsClosed s → IsClosed (f ⁻¹' s)

theorem IsClosed.preimage {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {t : Set Y} (h : IsClosed t) :

IsClosed (f ⁻¹' t)

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

f x ∈ closure (f '' s)

theorem continuousAt_iff_ultrafilter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {x : X} :

ContinuousAt f x ↔ ∀ (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))

theorem continuous_iff_ultrafilter {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} :

Continuous f ↔ ∀ (x : X) (g : Ultrafilter X), ↑g ≤ nhds x → Filter.Tendsto f (↑g) (nhds (f x))

theorem Continuous.closure_preimage_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (t : Set Y) :

closure (f ⁻¹' t) ⊆ f ⁻¹' closure t

theorem Continuous.frontier_preimage_subset {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (t : Set Y) :

frontier (f ⁻¹' t) ⊆ f ⁻¹' frontier t

theorem Set.MapsTo.closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y} (h : Set.MapsTo f s t) (hc : Continuous f) :

Set.MapsTo f (closure s) (closure t)

If a continuous map f maps s to t, then it maps closure s to closure t.

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

f '' closure s ⊆ closure (f '' s)

See also IsClosedMap.closure_image_eq_of_continuous.

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

closure (f '' closure s) = closure (f '' s)

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

closure s ⊆ f ⁻¹' closure (f '' s)

theorem map_mem_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {x : X} {t : Set Y} (hf : Continuous f) (hx : x ∈ closure s) (ht : Set.MapsTo f s t) :

f x ∈ closure t

theorem Set.MapsTo.closure_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} {s : Set X} {t : Set Y} (h : Set.MapsTo f s t) (hc : Continuous f) (ht : IsClosed t) :

Set.MapsTo f (closure s) t

If a continuous map f maps s to a closed set t, then it maps closure s to t.

theorem Filter.Tendsto.lift'_closure {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) {l : Filter X} {l' : Filter Y} (h : Filter.Tendsto f l l') :

Filter.Tendsto f (l.lift' closure) (l'.lift' closure)

theorem tendsto_lift'_closure_nhds {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) (x : X) :

Filter.Tendsto f ((nhds x).lift' closure) ((nhds (f x)).lift' closure)

Function with dense range #

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

A surjective map has dense range.

theorem denseRange_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

@[simp]

theorem denseRange_subtype_val {X : Type u_1} [TopologicalSpace X] {p : X → Prop} :

DenseRange Subtype.val ↔ Dense {x : X | p x}

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

hf.some x = Classical.choice ⋯

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 : s.Nonempty) :

∃ (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