Documentation

Mathlib.Topology.Basic

Basic theory of topological spaces. #

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

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

Notation #

𝓝 x: the filter nhds x of neighborhoods of a point x;
𝓟 s: the principal filter of a set s;
𝓝[s] x: the filter nhdsWithin x s of neighborhoods of a point x within a set s;
𝓝[≤] x≤] x: the filter nhdsWithin x (Set.Iic x) of left-neighborhoods of x;
𝓝[≥] x≥] x: the filter nhdsWithin x (Set.Ici x) of right-neighborhoods of x;
𝓝[<] x: the filter nhdsWithin x (Set.Iio x) of punctured left-neighborhoods of x;
𝓝[>] x: the filter nhdsWithin x (Set.Ioi x) of punctured right-neighborhoods of x;
𝓝[≠] x≠] x: the filter nhdsWithin x {x}ᶜ of punctured neighborhoods of x.

Implementation notes #

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

References #

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

Tags #

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

Topological spaces #

class TopologicalSpace (α : Type u) :

A predicate saying that a set is an open set. Use IsOpen in the root namespace instead.
IsOpen : Set α → Prop
The set representing the whole space is an open set. Use isOpen_univ in the root namespace instead.
isOpen_univ : IsOpen Set.univ
The intersection of two open sets is an open set. Use IsOpen.inter instead.
isOpen_inter : (s t : Set α) → IsOpen s → IsOpen t → IsOpen (s ∩ t)
The union of a family of open sets is an open set. Use isOpen_unionₛ in the root namespace instead.
isOpen_unionₛ : (s : Set (Set α)) → ((t : Set α) → t ∈ s → IsOpen t) → IsOpen (⋃₀ s)

A topology on α.

Instances

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

TopologicalSpace α

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

Equations

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

def IsOpen {α : Type u} [inst : TopologicalSpace α] :

Set α → Prop

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

Equations

IsOpen = TopologicalSpace.IsOpen

def Topology.IsOpen_of :

Lean.ParserDescr

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

Equations

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

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

IsOpen s ↔ p s

theorem topologicalSpace_eq {α : Type u} {f : TopologicalSpace α} {g : TopologicalSpace α} :

IsOpen = IsOpen → f = g

@[simp]

theorem isOpen_univ {α : Type u} [inst : TopologicalSpace α] :

IsOpen Set.univ

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

IsOpen (s₁ ∩ s₂)

theorem isOpen_unionₛ {α : Type u} [inst : TopologicalSpace α] {s : Set (Set α)} (h : ∀ (t : Set α), t ∈ s → IsOpen t) :

IsOpen (⋃₀ s)

theorem topologicalSpace_eq_iff {α : Type u} {t : TopologicalSpace α} {t' : TopologicalSpace α} :

t = t' ↔ ∀ (s : Set α), IsOpen s ↔ IsOpen s

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

TopologicalSpace.IsOpen s = IsOpen s

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

IsOpen (Set.unionᵢ fun i => f i)

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

IsOpen (Set.unionᵢ fun i => Set.unionᵢ fun h => f i)

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

IsOpen (s₁ ∪ s₂)

@[simp]

theorem isOpen_empty {α : Type u} [inst : TopologicalSpace α] :

theorem isOpen_interₛ {α : Type u} [inst : TopologicalSpace α] {s : Set (Set α)} (hs : Set.Finite s) :

(∀ (t : Set α), t ∈ s → IsOpen t) → IsOpen (⋂₀ s)

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

IsOpen (Set.interᵢ fun i => Set.interᵢ fun h => f i)

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

IsOpen (Set.interᵢ fun i => s i)

theorem isOpen_interᵢ_prop {α : Type u} [inst : TopologicalSpace α] {p : Prop} {s : p → Set α} (h : ∀ (h : p), IsOpen (s h)) :

IsOpen (Set.interᵢ s)

theorem isOpen_binterᵢ_finset {α : Type u} {β : Type v} [inst : TopologicalSpace α] {s : Finset β} {f : β → Set α} (h : ∀ (i : β), i ∈ s → IsOpen (f i)) :

IsOpen (Set.interᵢ fun i => Set.interᵢ fun h => f i)

@[simp]

theorem isOpen_const {α : Type u} [inst : TopologicalSpace α] {p : Prop} :

IsOpen { _a | p }

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

IsOpen { a | p₁ a } → IsOpen { a | p₂ a } → IsOpen { a | p₁ a ∧ p₂ a }

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

The complement of a closed set is an open set.
isOpen_compl : IsOpen (sᶜ)

A set is closed if its complement is open

Instances

def Topology.IsClosed_of :

Lean.ParserDescr

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

Equations

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

@[simp]

theorem isOpen_compl_iff {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

IsOpen (sᶜ) ↔ IsClosed s

theorem isClosed_const {α : Type u} [inst : TopologicalSpace α] {p : Prop} :

IsClosed { _a | p }

@[simp]

theorem isClosed_empty {α : Type u} [inst : TopologicalSpace α] :

@[simp]

theorem isClosed_univ {α : Type u} [inst : TopologicalSpace α] :

IsClosed Set.univ

theorem IsClosed.union {α : Type u} {s₁ : Set α} {s₂ : Set α} [inst : TopologicalSpace α] :

IsClosed s₁ → IsClosed s₂ → IsClosed (s₁ ∪ s₂)

theorem isClosed_interₛ {α : Type u} [inst : TopologicalSpace α] {s : Set (Set α)} :

(∀ (t : Set α), t ∈ s → IsClosed t) → IsClosed (⋂₀ s)

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

IsClosed (Set.interᵢ fun i => f i)

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

IsClosed (Set.interᵢ fun i => Set.interᵢ fun h => f i)

@[simp]

theorem isClosed_compl_iff {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

IsClosed (sᶜ) ↔ IsOpen s

theorem IsOpen.isClosed_compl {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

IsOpen s → IsClosed (sᶜ)

Alias of the reverse direction of isClosed_compl_iff.

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

IsOpen (s \ t)

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

IsClosed (s₁ ∩ s₂)

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

IsClosed (s \ t)

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

IsClosed (Set.unionᵢ fun i => Set.unionᵢ fun h => f i)

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

IsClosed (Set.unionᵢ fun i => s i)

theorem isClosed_unionᵢ_prop {α : Type u} [inst : TopologicalSpace α] {p : Prop} {s : p → Set α} (h : ∀ (h : p), IsClosed (s h)) :

IsClosed (Set.unionᵢ s)

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

IsClosed { x | p x → q x }

theorem IsClosed.not {α : Type u} {p : α → Prop} [inst : TopologicalSpace α] :

IsClosed { a | p a } → IsOpen { a | ¬p a }

Interior of a set #

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

Set α

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

Equations

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

theorem mem_interior {α : Type u} [inst : TopologicalSpace α] {s : Set α} {x : α} :

x ∈ interior s ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t

@[simp]

theorem isOpen_interior {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

IsOpen (interior s)

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

interior s ⊆ s

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

t ⊆ interior s

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

theorem interior_eq_iff_isOpen {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

interior s = s ↔ IsOpen s

theorem subset_interior_iff_isOpen {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

s ⊆ interior s ↔ IsOpen s

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

s ⊆ interior t ↔ s ⊆ t

theorem subset_interior_iff {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

t ⊆ interior s ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s

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

interior s ⊆ interior t

@[simp]

theorem interior_empty {α : Type u} [inst : TopologicalSpace α] :

interior ∅ = ∅

@[simp]

theorem interior_univ {α : Type u} [inst : TopologicalSpace α] :

interior Set.univ = Set.univ

@[simp]

theorem interior_eq_univ {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

interior s = Set.univ ↔ s = Set.univ

@[simp]

theorem interior_interior {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

interior (interior s) = interior s

@[simp]

theorem interior_inter {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

interior (s ∩ t) = interior s ∩ interior t

@[simp]

theorem Finset.interior_interᵢ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_1} (s : Finset ι) (f : ι → Set α) :

interior (Set.interᵢ fun i => Set.interᵢ fun h => f i) = Set.interᵢ fun i => Set.interᵢ fun h => interior (f i)

@[simp]

theorem interior_interᵢ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_1} [inst : Finite ι] (f : ι → Set α) :

interior (Set.interᵢ fun i => f i) = Set.interᵢ fun i => interior (f i)

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

interior (s ∪ t) = interior s

theorem isOpen_iff_forall_mem_open {α : Type u} {s : Set α} [inst : TopologicalSpace α] :

IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ t, t ⊆ s ∧ IsOpen t ∧ x ∈ t

theorem interior_interᵢ_subset {α : Type u} {ι : Sort w} [inst : TopologicalSpace α] (s : ι → Set α) :

interior (Set.interᵢ fun i => s i) ⊆ Set.interᵢ fun i => interior (s i)

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

interior (Set.interᵢ fun i => Set.interᵢ fun j => s i j) ⊆ Set.interᵢ fun i => Set.interᵢ fun j => interior (s i j)

theorem interior_interₛ_subset {α : Type u} [inst : TopologicalSpace α] (S : Set (Set α)) :

interior (⋂₀ S) ⊆ Set.interᵢ fun s => Set.interᵢ fun h => interior s

Closure of a set #

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

Set α

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

Equations

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

@[simp]

theorem isClosed_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

IsClosed (closure s)

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

s ⊆ closure s

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

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

closure s ⊆ t

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

Disjoint (closure s) t

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

Disjoint s (closure t)

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

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

closure s ⊆ s

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

closure s ⊆ t ↔ s ⊆ t

theorem IsClosed.mem_iff_closure_subset {α : Type u} [inst : TopologicalSpace α] {s : Set α} (hs : IsClosed s) {x : α} :

x ∈ s ↔ closure {x} ⊆ s

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

closure s ⊆ closure t

theorem monotone_closure (α : Type u_1) [inst : TopologicalSpace α] :

Monotone closure

theorem diff_subset_closure_iff {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

s \ t ⊆ closure t ↔ s ⊆ closure t

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

closure (s ∩ t) ⊆ closure s ∩ closure t

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

theorem closure_eq_iff_isClosed {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

closure s = s ↔ IsClosed s

theorem closure_subset_iff_isClosed {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

closure s ⊆ s ↔ IsClosed s

@[simp]

theorem closure_empty {α : Type u} [inst : TopologicalSpace α] :

closure ∅ = ∅

@[simp]

theorem closure_empty_iff {α : Type u} [inst : TopologicalSpace α] (s : Set α) :

closure s = ∅ ↔ s = ∅

@[simp]

theorem closure_nonempty_iff {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

Set.Nonempty (closure s) ↔ Set.Nonempty s

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

Set.Nonempty s → Set.Nonempty (closure s)

Alias of the reverse direction of closure_nonempty_iff.

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

Set.Nonempty (closure s) → Set.Nonempty s

Alias of the forward direction of closure_nonempty_iff.

@[simp]

theorem closure_univ {α : Type u} [inst : TopologicalSpace α] :

closure Set.univ = Set.univ

@[simp]

theorem closure_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

closure (closure s) = closure s

@[simp]

theorem closure_union {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

closure (s ∪ t) = closure s ∪ closure t

@[simp]

theorem Finset.closure_bunionᵢ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_1} (s : Finset ι) (f : ι → Set α) :

closure (Set.unionᵢ fun i => Set.unionᵢ fun h => f i) = Set.unionᵢ fun i => Set.unionᵢ fun h => closure (f i)

@[simp]

theorem closure_unionᵢ {α : Type u} [inst : TopologicalSpace α] {ι : Type u_1} [inst : Finite ι] (f : ι → Set α) :

closure (Set.unionᵢ fun i => f i) = Set.unionᵢ fun i => closure (f i)

theorem interior_subset_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

interior s ⊆ closure s

theorem closure_eq_compl_interior_compl {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

closure s = interior (sᶜ)ᶜ

@[simp]

theorem interior_compl {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

interior (sᶜ) = closure sᶜ

@[simp]

theorem closure_compl {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

closure (sᶜ) = interior sᶜ

theorem mem_closure_iff {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

a ∈ closure s ↔ ∀ (o : Set α), IsOpen o → a ∈ o → Set.Nonempty (o ∩ s)

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

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

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

l ≤ Filter.lift' l closure

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

Filter.HasBasis (Filter.lift' l closure) p fun i => closure (s i)

theorem Filter.HasBasis.lift'_closure_eq_self {α : Type u} {ι : Sort w} [inst : TopologicalSpace α] {l : Filter α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis l p s) (hc : ∀ (i : ι), p i → IsClosed (s i)) :

Filter.lift' l closure = l

@[simp]

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

Filter.lift' l closure = ⊥ ↔ l = ⊥

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

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

Equations

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

theorem dense_iff_closure_eq {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

Dense s ↔ closure s = Set.univ

theorem Dense.closure_eq {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

Dense s → closure s = Set.univ

Alias of the forward direction of dense_iff_closure_eq.

theorem interior_eq_empty_iff_dense_compl {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

interior s = ∅ ↔ Dense (sᶜ)

theorem Dense.interior_compl {α : Type u} [inst : TopologicalSpace α] {s : Set α} (h : Dense s) :

interior (sᶜ) = ∅

@[simp]

theorem dense_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

Dense (closure s) ↔ Dense s

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

theorem Dense.closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} (h : Dense s) :

Dense (closure s)

theorem Dense.of_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

Dense (closure s) → Dense s

Alias of the forward direction of dense_closure.

@[simp]

theorem dense_univ {α : Type u} [inst : TopologicalSpace α] :

Dense Set.univ

theorem dense_iff_inter_open {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

Dense s ↔ ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)

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

theorem Dense.inter_open_nonempty {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

Dense s → ∀ (U : Set α), IsOpen U → Set.Nonempty U → Set.Nonempty (U ∩ s)

Alias of the forward direction of dense_iff_inter_open.

theorem Dense.exists_mem_open {α : Type u} [inst : TopologicalSpace α] {s : Set α} (hs : Dense s) {U : Set α} (ho : IsOpen U) (hne : Set.Nonempty U) :

∃ x, x ∈ s ∧ x ∈ U

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

Set.Nonempty s ↔ Nonempty α

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

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

Dense s₂

theorem dense_compl_singleton_iff_not_open {α : Type u} [inst : TopologicalSpace α] {x : α} :

Dense ({x}ᶜ) ↔ ¬IsOpen {x}

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

Frontier of a set #

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

Set α

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

Equations

frontier s = closure s \ interior s

@[simp]

theorem closure_diff_interior {α : Type u} [inst : TopologicalSpace α] (s : Set α) :

closure s \ interior s = frontier s

@[simp]

theorem closure_diff_frontier {α : Type u} [inst : TopologicalSpace α] (s : Set α) :

closure s \ frontier s = interior s

@[simp]

theorem self_diff_frontier {α : Type u} [inst : TopologicalSpace α] (s : Set α) :

s \ frontier s = interior s

theorem frontier_eq_closure_inter_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

frontier s = closure s ∩ closure (sᶜ)

theorem frontier_subset_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

frontier s ⊆ closure s

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

frontier s ⊆ s

theorem frontier_closure_subset {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

frontier (closure s) ⊆ frontier s

theorem frontier_interior_subset {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

frontier (interior s) ⊆ frontier s

@[simp]

theorem frontier_compl {α : Type u} [inst : TopologicalSpace α] (s : Set α) :

frontier (sᶜ) = frontier s

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

@[simp]

theorem frontier_univ {α : Type u} [inst : TopologicalSpace α] :

frontier Set.univ = ∅

@[simp]

theorem frontier_empty {α : Type u} [inst : TopologicalSpace α] :

frontier ∅ = ∅

theorem frontier_inter_subset {α : Type u} [inst : TopologicalSpace α] (s : Set α) (t : Set α) :

frontier (s ∩ t) ⊆ frontier s ∩ closure t ∪ closure s ∩ frontier t

theorem frontier_union_subset {α : Type u} [inst : TopologicalSpace α] (s : Set α) (t : Set α) :

frontier (s ∪ t) ⊆ frontier s ∩ closure (tᶜ) ∪ closure (sᶜ) ∩ frontier t

theorem IsClosed.frontier_eq {α : Type u} [inst : TopologicalSpace α] {s : Set α} (hs : IsClosed s) :

frontier s = s \ interior s

theorem IsOpen.frontier_eq {α : Type u} [inst : TopologicalSpace α] {s : Set α} (hs : IsOpen s) :

frontier s = closure s \ s

theorem IsOpen.inter_frontier_eq {α : Type u} [inst : TopologicalSpace α] {s : Set α} (hs : IsOpen s) :

s ∩ frontier s = ∅

theorem isClosed_frontier {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

IsClosed (frontier s)

The frontier of a set is closed.

theorem interior_frontier {α : Type u} [inst : TopologicalSpace α] {s : Set α} (h : IsClosed s) :

interior (frontier s) = ∅

The frontier of a closed set has no interior point.

theorem closure_eq_interior_union_frontier {α : Type u} [inst : TopologicalSpace α] (s : Set α) :

closure s = interior s ∪ frontier s

theorem closure_eq_self_union_frontier {α : Type u} [inst : TopologicalSpace α] (s : Set α) :

closure s = s ∪ frontier s

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

Disjoint (frontier s) t

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

Disjoint s (frontier t)

theorem frontier_eq_inter_compl_interior {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

frontier s = interior sᶜ ∩ interior (sᶜ)ᶜ

theorem compl_frontier_eq_union_interior {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

frontier sᶜ = interior s ∪ interior (sᶜ)

Neighborhoods #

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

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

Equations

@nhds = @Wrapper.value✝ wrapped✝

theorem nhds_def {α : Type u_1} [inst : TopologicalSpace α] (a : α) :

nhds a = ⨅ s, ⨅ h, Filter.principal s

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

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

Equations

nhdsWithin a s = nhds a ⊓ Filter.principal s

def Topology.term𝓝 :

Lean.ParserDescr

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

Equations

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

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

Lean.ParserDescr

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

Equations

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

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

Lean.ParserDescr

Notation for the filter of punctured neighborhoods of a point.

Equations

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

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

Lean.ParserDescr

Notation for the filter of right neighborhoods of a point.

Equations

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

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

Lean.ParserDescr

Notation for the filter of left neighborhoods of a point.

Equations

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

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

Lean.ParserDescr

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

Equations

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

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

Lean.ParserDescr

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

Equations

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

theorem nhds_def' {α : Type u} [inst : TopologicalSpace α] (a : α) :

nhds a = ⨅ s, ⨅ _hs, ⨅ _ha, Filter.principal s

theorem nhds_basis_opens {α : Type u} [inst : TopologicalSpace α] (a : α) :

Filter.HasBasis (nhds a) (fun s => a ∈ s ∧ IsOpen s) fun s => s

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

theorem nhds_basis_closeds {α : Type u} [inst : TopologicalSpace α] (a : α) :

Filter.HasBasis (nhds a) (fun s => ¬a ∈ s ∧ IsClosed s) compl

theorem le_nhds_iff {α : Type u} [inst : TopologicalSpace α] {f : Filter α} {a : α} :

f ≤ nhds a ↔ ∀ (s : Set α), a ∈ s → IsOpen s → s ∈ f

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

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

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

theorem mem_nhds_iff {α : Type u} [inst : TopologicalSpace α] {a : α} {s : Set α} :

s ∈ nhds a ↔ ∃ t, t ⊆ s ∧ IsOpen t ∧ a ∈ t

theorem eventually_nhds_iff {α : Type u} [inst : TopologicalSpace α] {a : α} {p : α → Prop} :

Filter.Eventually (fun x => p x) (nhds a) ↔ ∃ t, ((x : α) → x ∈ t → p x) ∧ IsOpen t ∧ a ∈ t

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

theorem mem_interior_iff_mem_nhds {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

a ∈ interior s ↔ s ∈ nhds a

theorem map_nhds {α : Type u} {β : Type v} [inst : TopologicalSpace α] {a : α} {f : α → β} :

Filter.map f (nhds a) = ⨅ s, ⨅ h, Filter.principal (f '' s)

theorem mem_of_mem_nhds {α : Type u} [inst : TopologicalSpace α] {a : α} {s : Set α} :

s ∈ nhds a → a ∈ s

theorem Filter.Eventually.self_of_nhds {α : Type u} [inst : TopologicalSpace α] {p : α → Prop} {a : α} (h : Filter.Eventually (fun y => p y) (nhds a)) :

p a

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

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

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

s ∈ nhds a ↔ a ∈ s

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

sᶜ ∈ nhds a

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

Filter.Eventually (fun x => x ∈ s) (nhds a)

theorem nhds_basis_opens' {α : Type u} [inst : TopologicalSpace α] (a : α) :

Filter.HasBasis (nhds a) (fun s => s ∈ nhds a ∧ IsOpen s) fun x => x

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

theorem exists_open_set_nhds {α : Type u} [inst : TopologicalSpace α] {s : Set α} {U : Set α} (h : ∀ (x : α), x ∈ s → U ∈ nhds x) :

∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U

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

theorem exists_open_set_nhds' {α : Type u} [inst : TopologicalSpace α] {s : Set α} {U : Set α} (h : U ∈ ⨆ x, ⨆ h, nhds x) :

∃ V, s ⊆ V ∧ IsOpen V ∧ V ⊆ U

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

theorem Filter.Eventually.eventually_nhds {α : Type u} [inst : TopologicalSpace α] {p : α → Prop} {a : α} (h : Filter.Eventually (fun y => p y) (nhds a)) :

Filter.Eventually (fun y => Filter.Eventually (fun x => p x) (nhds y)) (nhds a)

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

@[simp]

theorem eventually_eventually_nhds {α : Type u} [inst : TopologicalSpace α] {p : α → Prop} {a : α} :

Filter.Eventually (fun y => Filter.Eventually (fun x => p x) (nhds y)) (nhds a) ↔ Filter.Eventually (fun x => p x) (nhds a)

@[simp]

theorem frequently_frequently_nhds {α : Type u} [inst : TopologicalSpace α] {p : α → Prop} {a : α} :

Filter.Frequently (fun y => Filter.Frequently (fun x => p x) (nhds y)) (nhds a) ↔ Filter.Frequently (fun x => p x) (nhds a)

@[simp]

theorem eventually_mem_nhds {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

Filter.Eventually (fun x => s ∈ nhds x) (nhds a) ↔ s ∈ nhds a

@[simp]

theorem nhds_bind_nhds {α : Type u} {a : α} [inst : TopologicalSpace α] :

Filter.bind (nhds a) nhds = nhds a

@[simp]

theorem eventually_eventuallyEq_nhds {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : α → β} {g : α → β} {a : α} :

Filter.Eventually (fun y => f =ᶠ[nhds y] g) (nhds a) ↔ f =ᶠ[nhds a] g

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

f a = g a

@[simp]

theorem eventually_eventuallyLE_nhds {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst : LE β] {f : α → β} {g : α → β} {a : α} :

Filter.Eventually (fun y => f ≤ᶠ[nhds y] g) (nhds a) ↔ f ≤ᶠ[nhds a] g

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

Filter.Eventually (fun y => f =ᶠ[nhds y] g) (nhds a)

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

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

Filter.Eventually (fun y => f ≤ᶠ[nhds y] g) (nhds a)

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

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

((s : Set α) → s ∈ nhds x → P s) ↔ (s : Set α) → IsOpen s → x ∈ s → P s

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

(∀ (s : Set α), s ∈ nhds x → f s ∈ l) ↔ ∀ (s : Set α), IsOpen s → x ∈ s → f s ∈ l

theorem tendsto_nhds {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : β → α} {l : Filter β} {a : α} :

Filter.Tendsto f l (nhds a) ↔ ∀ (s : Set α), IsOpen s → a ∈ s → f ⁻¹' s ∈ l

theorem tendsto_atTop_nhds {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst : Nonempty β] [inst : SemilatticeSup β] {f : β → α} {a : α} :

Filter.Tendsto f Filter.atTop (nhds a) ↔ ∀ (U : Set α), a ∈ U → IsOpen U → ∃ N, ∀ (n : β), N ≤ n → f n ∈ U

theorem tendsto_const_nhds {α : Type u} {β : Type v} [inst : TopologicalSpace α] {a : α} {f : Filter β} :

Filter.Tendsto (fun x => a) f (nhds a)

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

Filter.Tendsto u Filter.atTop (nhds x)

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

Filter.Tendsto u Filter.atBot (nhds x)

theorem pure_le_nhds {α : Type u} [inst : TopologicalSpace α] :

pure ≤ nhds

theorem tendsto_pure_nhds {β : Type v} {α : Type u_1} [inst : TopologicalSpace β] (f : α → β) (a : α) :

Filter.Tendsto f (pure a) (nhds (f a))

theorem OrderTop.tendsto_atTop_nhds {β : Type v} {α : Type u_1} [inst : PartialOrder α] [inst : OrderTop α] [inst : TopologicalSpace β] (f : α → β) :

Filter.Tendsto f Filter.atTop (nhds (f ⊤))

@[simp]

instance nhds_neBot {α : Type u} [inst : TopologicalSpace α] {a : α} :

Filter.NeBot (nhds a)

Equations

@nhds_neBot = @nhds_neBot.proof_1

Cluster points #

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

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

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

Equations

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

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

Filter.NeBot (nhds x ⊓ F)

theorem Filter.HasBasis.clusterPt_iff {α : Type u} {a : α} [inst : TopologicalSpace α] {ιa : Sort u_1} {ιF : Sort u_2} {pa : ιa → Prop} {sa : ιa → Set α} {pF : ιF → Prop} {sF : ιF → Set α} {F : Filter α} (ha : Filter.HasBasis (nhds a) pa sa) (hF : Filter.HasBasis F pF sF) :

ClusterPt a F ↔ ∀ ⦃i : ιa⦄, pa i → ∀ ⦃j : ιF⦄, pF j → Set.Nonempty (sa i ∩ sF j)

theorem clusterPt_iff {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Filter α} :

ClusterPt x F ↔ ∀ ⦃U : Set α⦄, U ∈ nhds x → ∀ ⦃V : Set α⦄, V ∈ F → Set.Nonempty (U ∩ V)

theorem clusterPt_iff_not_disjoint {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Filter α} :

ClusterPt x F ↔ ¬Disjoint (nhds x) F

theorem clusterPt_principal_iff {α : Type u} [inst : TopologicalSpace α] {x : α} {s : Set α} :

ClusterPt x (Filter.principal s) ↔ ∀ (U : Set α), U ∈ nhds x → Set.Nonempty (U ∩ s)

x is a cluster point of a set s if every neighbourhood of x meets s on a nonempty set. See also mem_closure_iff_clusterPt.

theorem clusterPt_principal_iff_frequently {α : Type u} [inst : TopologicalSpace α] {x : α} {s : Set α} :

ClusterPt x (Filter.principal s) ↔ Filter.Frequently (fun y => y ∈ s) (nhds x)

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

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

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

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

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

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

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

ClusterPt x ↑f ↔ ↑f ≤ nhds x

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

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

Equations

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

theorem mapClusterPt_iff {α : Type u} [inst : TopologicalSpace α] {ι : Type u_1} (x : α) (F : Filter ι) (u : ι → α) :

MapClusterPt x F u ↔ ∀ (s : Set α), s ∈ nhds x → Filter.Frequently (fun a => u a ∈ s) F

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

MapClusterPt x F u

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

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

Equations

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

theorem acc_iff_cluster {α : Type u} [inst : TopologicalSpace α] (x : α) (F : Filter α) :

AccPt x F ↔ ClusterPt x (Filter.principal ({x}ᶜ) ⊓ F)

theorem acc_principal_iff_cluster {α : Type u} [inst : TopologicalSpace α] (x : α) (C : Set α) :

AccPt x (Filter.principal C) ↔ ClusterPt x (Filter.principal (C \ {x}))

x is an accumulation point of a set C iff it is a cluster point of C ∖ {x}∖ {x}.

theorem accPt_iff_nhds {α : Type u} [inst : TopologicalSpace α] (x : α) (C : Set α) :

AccPt x (Filter.principal C) ↔ ∀ (U : Set α), U ∈ nhds x → ∃ y, y ∈ U ∩ C ∧ y ≠ x

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

theorem accPt_iff_frequently {α : Type u} [inst : TopologicalSpace α] (x : α) (C : Set α) :

AccPt x (Filter.principal C) ↔ Filter.Frequently (fun y => y ≠ x ∧ y ∈ C) (nhds x)

x is an accumulation point of a set C iff there are points near x in C and different from x.

theorem AccPt.mono {α : Type u} [inst : TopologicalSpace α] {x : α} {F : Filter α} {G : Filter α} (h : AccPt x F) (hFG : F ≤ G) :

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

Interior, closure and frontier in terms of neighborhoods #

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

interior s = { a | s ∈ nhds a }

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

interior s = { a | nhds a ≤ Filter.principal s }

@[simp]

theorem interior_mem_nhds {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

interior s ∈ nhds a ↔ s ∈ nhds a

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

interior { x | p x } = { x | Filter.Eventually (fun y => p y) (nhds x) }

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

IsOpen { x | Filter.Eventually (fun y => p y) (nhds x) }

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

s ⊆ interior V ↔ ∀ (x : α), x ∈ s → V ∈ nhds x

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

IsOpen s ↔ ∀ (a : α), a ∈ s → nhds a ≤ Filter.principal s

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

IsOpen s ↔ ∀ (a : α), a ∈ s → s ∈ nhds a

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

IsOpen s ↔ ∀ (x : α), x ∈ s → Filter.Eventually (fun y => y ∈ s) (nhds x)

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

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

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

theorem isOpen_singleton_iff_nhds_eq_pure {α : Type u} [inst : TopologicalSpace α] (a : α) :

IsOpen {a} ↔ nhds a = pure a

theorem isOpen_singleton_iff_punctured_nhds {α : Type u_1} [inst : TopologicalSpace α] (a : α) :

IsOpen {a} ↔ nhdsWithin a ({a}ᶜ) = ⊥

theorem mem_closure_iff_frequently {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

a ∈ closure s ↔ Filter.Frequently (fun x => x ∈ s) (nhds a)

theorem Filter.Frequently.mem_closure {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

Filter.Frequently (fun x => x ∈ s) (nhds a) → a ∈ closure s

Alias of the reverse direction of mem_closure_iff_frequently.

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

IsClosed s ↔ ∀ (x : α), Filter.Frequently (fun y => y ∈ s) (nhds x) → x ∈ s

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

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

IsClosed { x | ClusterPt x f }

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

theorem mem_closure_iff_clusterPt {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

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

theorem mem_closure_iff_nhds_neBot {α : Type u} {a : α} [inst : TopologicalSpace α] {s : Set α} :

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

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

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

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

closure ({x}ᶜ) = Set.univ

If x is not an isolated point of a topological space, then the closure of {x}ᶜ is the whole space.

@[simp]

theorem interior_singleton {α : Type u} [inst : TopologicalSpace α] (x : α) [inst : Filter.NeBot (nhdsWithin x ({x}ᶜ))] :

interior {x} = ∅

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

theorem not_isOpen_singleton {α : Type u} [inst : TopologicalSpace α] (x : α) [inst : Filter.NeBot (nhdsWithin x ({x}ᶜ))] :

theorem closure_eq_cluster_pts {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

closure s = { a | ClusterPt a (Filter.principal s) }

theorem mem_closure_iff_nhds {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

a ∈ closure s ↔ ∀ (t : Set α), t ∈ nhds a → Set.Nonempty (t ∩ s)

theorem mem_closure_iff_nhds' {α : Type u} [inst : TopologicalSpace α] {s : Set α} {a : α} :

a ∈ closure s ↔ ∀ (t : Set α), t ∈ nhds a → ∃ y, ↑y ∈ t

theorem mem_closure_iff_comap_neBot {α : Type u} [inst : TopologicalSpace α] {A : Set α} {x : α} :

x ∈ closure A ↔ Filter.NeBot (Filter.comap Subtype.val (nhds x))

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

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

theorem mem_closure_iff_nhds_basis {α : Type u} {ι : Sort w} [inst : TopologicalSpace α] {a : α} {p : ι → Prop} {s : ι → Set α} (h : Filter.HasBasis (nhds a) p s) {t : Set α} :

a ∈ closure t ↔ ∀ (i : ι), p i → ∃ y, y ∈ t ∧ y ∈ s i

theorem mem_closure_iff_ultrafilter {α : Type u} [inst : TopologicalSpace α] {s : Set α} {x : α} :

x ∈ closure s ↔ ∃ u, s ∈ u ∧ ↑u ≤ nhds x

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

theorem isClosed_iff_clusterPt {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

IsClosed s ↔ ∀ (a : α), ClusterPt a (Filter.principal s) → a ∈ s

theorem isClosed_iff_nhds {α : Type u} [inst : TopologicalSpace α] {s : Set α} :

IsClosed s ↔ ∀ (x : α), (∀ (U : Set α), U ∈ nhds x → Set.Nonempty (U ∩ s)) → x ∈ s

theorem IsClosed.interior_union_left {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

IsClosed s → interior (s ∪ t) ⊆ s ∪ interior t

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

interior (s ∪ t) ⊆ interior s ∪ t

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

s ∩ closure t ⊆ closure (s ∩ t)

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

closure s ∩ t ⊆ closure (s ∩ t)

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

t ⊆ closure (t ∩ s)

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

x ∈ closure s₂

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

Dense (s ∩ t)

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

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

Dense (s ∩ t)

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

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

Set.Nonempty (s ∩ t)

theorem closure_diff {α : Type u} [inst : TopologicalSpace α] {s : Set α} {t : Set α} :

closure s \ closure t ⊆ closure (s \ t)

theorem Filter.Frequently.mem_of_closed {α : Type u} [inst : TopologicalSpace α] {a : α} {s : Set α} (h : Filter.Frequently (fun x => x ∈ s) (nhds a)) (hs : IsClosed s) :

a ∈ s

theorem IsClosed.mem_of_frequently_of_tendsto {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : β → α} {b : Filter β} {a : α} {s : Set α} (hs : IsClosed s) (h : Filter.Frequently (fun x => f x ∈ s) b) (hf : Filter.Tendsto f b (nhds a)) :

a ∈ s

theorem IsClosed.mem_of_tendsto {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : β → α} {b : Filter β} {a : α} {s : Set α} [inst : Filter.NeBot b] (hs : IsClosed s) (hf : Filter.Tendsto f b (nhds a)) (h : Filter.Eventually (fun x => f x ∈ s) b) :

a ∈ s

theorem mem_closure_of_frequently_of_tendsto {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : β → α} {b : Filter β} {a : α} {s : Set α} (h : Filter.Frequently (fun x => f x ∈ s) b) (hf : Filter.Tendsto f b (nhds a)) :

a ∈ closure s

theorem mem_closure_of_tendsto {α : Type u} {β : Type v} [inst : TopologicalSpace α] {f : β → α} {b : Filter β} {a : α} {s : Set α} [inst : Filter.NeBot b] (hf : Filter.Tendsto f b (nhds a)) (h : Filter.Eventually (fun x => f x ∈ s) b) :

a ∈ closure s

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

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

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

Limits of filters in topological spaces #

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

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

α

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

Equations

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

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

α

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

Equations

Ultrafilter.lim F = lim ↑F

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

α

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

Equations

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

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

f ≤ nhds (lim f)

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

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

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

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

Continuity #

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

The preimage of an open set under a continuous function is an open set. Use IsOpen.preimage instead.
isOpen_preimage : ∀ (s : Set β), IsOpen s → IsOpen (f ⁻¹' s)

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

Instances For

def Topology.Continuous_of :

Lean.ParserDescr

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

Equations

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

theorem continuous_def {α : Type u_1} {β : Type u_2} :

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

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

IsOpen (f ⁻¹' s)

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

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

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

Equations

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

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

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

theorem continuousAt_def {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} {x : α} :

ContinuousAt f x ↔ ∀ (A : Set β), A ∈ nhds (f x) → f ⁻¹' A ∈ nhds x

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

ContinuousAt f x ↔ ContinuousAt g x

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

ContinuousAt g x

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

f ⁻¹' t ∈ nhds x

theorem eventuallyEq_zero_nhds {α : Type u_2} [inst : TopologicalSpace α] {M₀ : Type u_1} [inst : Zero M₀] {a : α} {f : α → M₀} :

f =ᶠ[nhds a] 0 ↔ ¬a ∈ closure (Function.support f)

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

ClusterPt (f x) lb

theorem preimage_interior_subset_interior_preimage {α : Type u_2} {β : Type u_1} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} {s : Set β} (hf : Continuous f) :

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

See also interior_preimage_subset_preimage_interior.

theorem continuous_id {α : Type u_1} [inst : TopologicalSpace α] :

theorem continuous_id' {α : Type u_1} [inst : TopologicalSpace α] :

Continuous fun x => x

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

Continuous (g ∘ f)

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

Continuous fun x => g (f x)

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

Continuous (f^[n])

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

ContinuousAt (g ∘ f) x

theorem Continuous.tendsto {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} (hf : Continuous f) (x : α) :

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

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

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

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

theorem Continuous.continuousAt {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} {x : α} (h : Continuous f) :

ContinuousAt f x

theorem continuous_iff_continuousAt {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} :

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

theorem continuousAt_const {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {x : α} {b : β} :

ContinuousAt (fun x => b) x

theorem continuous_const {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {b : β} :

Continuous fun x => b

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

ContinuousAt f x

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

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

ContinuousAt id x

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

ContinuousAt (f^[n]) x

theorem continuous_iff_isClosed {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} :

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

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

IsClosed (f ⁻¹' s)

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

f x ∈ closure (f '' s)

theorem continuousAt_iff_ultrafilter {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} {x : α} :

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

theorem continuous_iff_ultrafilter {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} :

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

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

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

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

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

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

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

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

theorem image_closure_subset_closure_image {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) :

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

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

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

theorem closure_subset_preimage_closure_image {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst : TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) :

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

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

f a ∈ closure t

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

Set.MapsTo f (closure s) t

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

Function with dense range #

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

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

Equations

DenseRange f = Dense (Set.range f)

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

A surjective map has dense range.

theorem denseRange_id {α : Type u_1} [inst : TopologicalSpace α] :

theorem denseRange_iff_closure_range {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κ → β} :

DenseRange f ↔ closure (Set.range f) = Set.univ

theorem DenseRange.closure_range {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κ → β} (h : DenseRange f) :

closure (Set.range f) = Set.univ

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

DenseRange Subtype.val

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

Set.range f ⊆ closure (f '' s)

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

Dense (f '' s)

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

theorem DenseRange.subset_closure_image_preimage_of_isOpen {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κ → β} (hf : DenseRange f) {s : Set β} (hs : IsOpen s) :

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

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

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

DenseRange (g ∘ f)

Composition of a continuous map with dense range and a function with dense range has dense range.

theorem DenseRange.nonempty_iff {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κ → β} (hf : DenseRange f) :

Nonempty κ ↔ Nonempty β

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

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

κ

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

Equations

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

theorem DenseRange.exists_mem_open {β : Type u_1} [inst : TopologicalSpace β] {κ : Type u_2} {f : κ → β} (hf : DenseRange f) {s : Set β} (ho : IsOpen s) (hs : Set.Nonempty s) :

∃ a, f a ∈ s

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

∃ a, f a ∈ U