mathlib docs: topology.basic

source

@[class]

structure topological_space :

Type u → Type u

is_open : set α → Prop
is_open_univ : c.is_open set.univ
is_open_inter : ∀ (s t : set α), c.is_open s → c.is_open t → c.is_open (s ∩ t)
is_open_sUnion : ∀ (s : set (set α)), (∀ (t : set α), t ∈ s → c.is_open t) → c.is_open (⋃₀s)

A topology on α.

Instances

source

def topological_space.of_closed {α : Type u} (T : set (set α)) :

∅ ∈ T → (∀ (A : set (set α)), A ⊆ T → ⋂₀A ∈ T) → (∀ (A B : set α), A ∈ T → B ∈ T → A ∪ B ∈ T) → topological_space α

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

Equations

topological_space.of_closed T empty_mem sInter_mem union_mem = {is_open := λ (X : set α), Xᶜ ∈ T, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}

source

@[ext]

theorem topological_space_eq {α : Type u} {f g : topological_space α} :

f.is_open = g.is_open → f = g

source

def is_open {α : Type u} [t : topological_space α] :

set α → Prop

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

Equations

is_open s = t.is_open s

source

@[simp]

theorem is_open_univ {α : Type u} [t : topological_space α] :

is_open set.univ

source

theorem is_open_inter {α : Type u} {s₁ s₂ : set α} [t : topological_space α] :

is_open s₁ → is_open s₂ → is_open (s₁ ∩ s₂)

source

theorem is_open_sUnion {α : Type u} [t : topological_space α] {s : set (set α)} :

(∀ (t_1 : set α), t_1 ∈ s → is_open t_1) → is_open (⋃₀s)

source

theorem is_open_fold {α : Type u} {s : set α} {t : topological_space α} :

t.is_open s = is_open s

source

theorem is_open_Union {α : Type u} {ι : Sort w} [topological_space α] {f : ι → set α} :

(∀ (i : ι), is_open (f i)) → is_open (⋃ (i : ι), f i)

source

theorem is_open_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} :

(∀ (i : β), i ∈ s → is_open (f i)) → is_open (⋃ (i : β) (H : i ∈ s), f i)

source

theorem is_open_union {α : Type u} {s₁ s₂ : set α} [topological_space α] :

is_open s₁ → is_open s₂ → is_open (s₁ ∪ s₂)

source

@[simp]

theorem is_open_empty {α : Type u} [topological_space α] :

is_open ∅

source

theorem is_open_sInter {α : Type u} [topological_space α] {s : set (set α)} :

s.finite → (∀ (t : set α), t ∈ s → is_open t) → is_open (⋂₀s)

source

theorem is_open_bInter {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} :

s.finite → (∀ (i : β), i ∈ s → is_open (f i)) → is_open (⋂ (i : β) (H : i ∈ s), f i)

source

theorem is_open_Inter {α : Type u} {β : Type v} [topological_space α] [fintype β] {s : β → set α} :

(∀ (i : β), is_open (s i)) → is_open (⋂ (i : β), s i)

source

theorem is_open_Inter_prop {α : Type u} [topological_space α] {p : Prop} {s : p → set α} :

(∀ (h : p), is_open (s h)) → is_open (set.Inter s)

source

theorem is_open_const {α : Type u} [topological_space α] {p : Prop} :

is_open {a : α | p}

source

theorem is_open_and {α : Type u} {p₁ p₂ : α → Prop} [topological_space α] :

is_open {a : α | p₁ a} → is_open {a : α | p₂ a} → is_open {a : α | p₁ a ∧ p₂ a}

source

def is_closed {α : Type u} [topological_space α] :

set α → Prop

A set is closed if its complement is open

Equations

is_closed s = is_open sᶜ

source

@[simp]

theorem is_closed_empty {α : Type u} [topological_space α] :

is_closed ∅

source

@[simp]

theorem is_closed_univ {α : Type u} [topological_space α] :

is_closed set.univ

source

theorem is_closed_union {α : Type u} {s₁ s₂ : set α} [topological_space α] :

is_closed s₁ → is_closed s₂ → is_closed (s₁ ∪ s₂)

source

theorem is_closed_sInter {α : Type u} [topological_space α] {s : set (set α)} :

(∀ (t : set α), t ∈ s → is_closed t) → is_closed (⋂₀s)

source

theorem is_closed_Inter {α : Type u} {ι : Sort w} [topological_space α] {f : ι → set α} :

(∀ (i : ι), is_closed (f i)) → is_closed (⋂ (i : ι), f i)

source

@[simp]

theorem is_open_compl_iff {α : Type u} [topological_space α] {s : set α} :

is_open sᶜ ↔ is_closed s

source

@[simp]

theorem is_closed_compl_iff {α : Type u} [topological_space α] {s : set α} :

is_closed sᶜ ↔ is_open s

source

theorem is_open_diff {α : Type u} [topological_space α] {s t : set α} :

is_open s → is_closed t → is_open (s \ t)

source

theorem is_closed_inter {α : Type u} {s₁ s₂ : set α} [topological_space α] :

is_closed s₁ → is_closed s₂ → is_closed (s₁ ∩ s₂)

source

theorem is_closed_bUnion {α : Type u} {β : Type v} [topological_space α] {s : set β} {f : β → set α} :

s.finite → (∀ (i : β), i ∈ s → is_closed (f i)) → is_closed (⋃ (i : β) (H : i ∈ s), f i)

source

theorem is_closed_Union {α : Type u} {β : Type v} [topological_space α] [fintype β] {s : β → set α} :

(∀ (i : β), is_closed (s i)) → is_closed (set.Union s)

source

theorem is_closed_Union_prop {α : Type u} [topological_space α] {p : Prop} {s : p → set α} :

(∀ (h : p), is_closed (s h)) → is_closed (set.Union s)

source

theorem is_closed_imp {α : Type u} [topological_space α] {p q : α → Prop} :

is_open {x : α | p x} → is_closed {x : α | q x} → is_closed {x : α | p x → q x}

source

theorem is_open_neg {α : Type u} {p : α → Prop} [topological_space α] :

is_closed {a : α | p a} → is_open {a : α | ¬p a}

source

def interior {α : Type u} [topological_space α] :

set α → set α

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

Equations

interior s = ⋃₀{t : set α | is_open t ∧ t ⊆ s}

source

theorem mem_interior {α : Type u} [topological_space α] {s : set α} {x : α} :

x ∈ interior s ↔ ∃ (t : set α) (H : t ⊆ s), is_open t ∧ x ∈ t

source

@[simp]

theorem is_open_interior {α : Type u} [topological_space α] {s : set α} :

is_open (interior s)

source

theorem interior_subset {α : Type u} [topological_space α] {s : set α} :

interior s ⊆ s

source

theorem interior_maximal {α : Type u} [topological_space α] {s t : set α} :

t ⊆ s → is_open t → t ⊆ interior s

source

theorem is_open.interior_eq {α : Type u} [topological_space α] {s : set α} :

is_open s → interior s = s

source

theorem interior_eq_iff_open {α : Type u} [topological_space α] {s : set α} :

interior s = s ↔ is_open s

source

theorem subset_interior_iff_open {α : Type u} [topological_space α] {s : set α} :

s ⊆ interior s ↔ is_open s

source

theorem subset_interior_iff_subset_of_open {α : Type u} [topological_space α] {s t : set α} :

is_open s → (s ⊆ interior t ↔ s ⊆ t)

source

theorem interior_mono {α : Type u} [topological_space α] {s t : set α} :

s ⊆ t → interior s ⊆ interior t

source

@[simp]

theorem interior_empty {α : Type u} [topological_space α] :

interior ∅ = ∅

source

@[simp]

theorem interior_univ {α : Type u} [topological_space α] :

interior set.univ = set.univ

source

@[simp]

theorem interior_interior {α : Type u} [topological_space α] {s : set α} :

interior (interior s) = interior s

source

@[simp]

theorem interior_inter {α : Type u} [topological_space α] {s t : set α} :

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

source

theorem interior_union_is_closed_of_interior_empty {α : Type u} [topological_space α] {s t : set α} :

is_closed s → interior t = ∅ → interior (s ∪ t) = interior s

source

theorem is_open_iff_forall_mem_open {α : Type u} {s : set α} [topological_space α] :

is_open s ↔ ∀ (x : α), x ∈ s → (∃ (t : set α) (H : t ⊆ s), is_open t ∧ x ∈ t)

source

def closure {α : Type u} [topological_space α] :

set α → set α

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

Equations

closure s = ⋂₀{t : set α | is_closed t ∧ s ⊆ t}

source

@[simp]

theorem is_closed_closure {α : Type u} [topological_space α] {s : set α} :

is_closed (closure s)

source

theorem subset_closure {α : Type u} [topological_space α] {s : set α} :

s ⊆ closure s

source

theorem closure_minimal {α : Type u} [topological_space α] {s t : set α} :

s ⊆ t → is_closed t → closure s ⊆ t

source

theorem is_closed.closure_eq {α : Type u} [topological_space α] {s : set α} :

is_closed s → closure s = s

source

theorem is_closed.closure_subset {α : Type u} [topological_space α] {s : set α} :

is_closed s → closure s ⊆ s

source

theorem is_closed.closure_subset_iff {α : Type u} [topological_space α] {s t : set α} :

is_closed t → (closure s ⊆ t ↔ s ⊆ t)

source

theorem closure_mono {α : Type u} [topological_space α] {s t : set α} :

s ⊆ t → closure s ⊆ closure t

source

theorem monotone_closure (α : Type u_1) [topological_space α] :

monotone closure

source

theorem closure_inter_subset_inter_closure {α : Type u} [topological_space α] (s t : set α) :

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

source

theorem is_closed_of_closure_subset {α : Type u} [topological_space α] {s : set α} :

closure s ⊆ s → is_closed s

source

theorem closure_eq_iff_is_closed {α : Type u} [topological_space α] {s : set α} :

closure s = s ↔ is_closed s

source

theorem closure_subset_iff_is_closed {α : Type u} [topological_space α] {s : set α} :

closure s ⊆ s ↔ is_closed s

source

@[simp]

theorem closure_empty {α : Type u} [topological_space α] :

closure ∅ = ∅

source

@[simp]

theorem closure_empty_iff {α : Type u} [topological_space α] (s : set α) :

closure s = ∅ ↔ s = ∅

source

theorem set.nonempty.closure {α : Type u} [topological_space α] {s : set α} :

s.nonempty → (closure s).nonempty

source

@[simp]

theorem closure_univ {α : Type u} [topological_space α] :

closure set.univ = set.univ

source

@[simp]

theorem closure_closure {α : Type u} [topological_space α] {s : set α} :

closure (closure s) = closure s

source

@[simp]

theorem closure_union {α : Type u} [topological_space α] {s t : set α} :

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

source

theorem interior_subset_closure {α : Type u} [topological_space α] {s : set α} :

interior s ⊆ closure s

source

theorem closure_eq_compl_interior_compl {α : Type u} [topological_space α] {s : set α} :

closure s = (interior sᶜ)ᶜ

source

@[simp]

theorem interior_compl {α : Type u} [topological_space α] {s : set α} :

interior sᶜ = (closure s)ᶜ

source

@[simp]

theorem closure_compl {α : Type u} [topological_space α] {s : set α} :

closure sᶜ = (interior s)ᶜ

source

theorem mem_closure_iff {α : Type u} [topological_space α] {s : set α} {a : α} :

a ∈ closure s ↔ ∀ (o : set α), is_open o → a ∈ o → (o ∩ s).nonempty

source

theorem dense_iff_inter_open {α : Type u} [topological_space α] {s : set α} :

closure s = set.univ ↔ ∀ (U : set α), is_open U → U.nonempty → (U ∩ s).nonempty

source

theorem dense_of_subset_dense {α : Type u} [topological_space α] {s₁ s₂ : set α} :

s₁ ⊆ s₂ → closure s₁ = set.univ → closure s₂ = set.univ

source

def frontier {α : Type u} [topological_space α] :

set α → set α

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

Equations

frontier s = closure s \ interior s

source

theorem frontier_eq_closure_inter_closure {α : Type u} [topological_space α] {s : set α} :

frontier s = closure s ∩ closure sᶜ

source

@[simp]

theorem frontier_compl {α : Type u} [topological_space α] (s : set α) :

frontier sᶜ = frontier s

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

source

theorem frontier_inter_subset {α : Type u} [topological_space α] (s t : set α) :

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

source

theorem frontier_union_subset {α : Type u} [topological_space α] (s t : set α) :

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

source

theorem is_closed.frontier_eq {α : Type u} [topological_space α] {s : set α} :

is_closed s → frontier s = s \ interior s

source

theorem is_open.frontier_eq {α : Type u} [topological_space α] {s : set α} :

is_open s → frontier s = closure s \ s

source

theorem is_closed_frontier {α : Type u} [topological_space α] {s : set α} :

is_closed (frontier s)

The frontier of a set is closed.

source

theorem interior_frontier {α : Type u} [topological_space α] {s : set α} :

is_closed s → interior (frontier s) = ∅

The frontier of a closed set has no interior point.

source

theorem closure_eq_interior_union_frontier {α : Type u} [topological_space α] (s : set α) :

closure s = interior s ∪ frontier s

source

theorem closure_eq_self_union_frontier {α : Type u} [topological_space α] (s : set α) :

closure s = s ∪ frontier s

source

def nhds {α : Type u} [topological_space α] :

α → filter α

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

Equations

nhds a = ⨅ (s : set α) (H : s ∈ {s : set α | a ∈ s ∧ is_open s}), filter.principal s

source

theorem nhds_def {α : Type u} [topological_space α] (a : α) :

nhds a = ⨅ (s : set α) (H : s ∈ {s : set α | a ∈ s ∧ is_open s}), filter.principal s

source

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

(nhds a).has_basis (λ (s : set α), a ∈ s ∧ is_open s) (λ (x : set α), x)

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

source

theorem le_nhds_iff {α : Type u} [topological_space α] {f : filter α} {a : α} :

f ≤ nhds a ↔ ∀ (s : set α), a ∈ s → is_open s → s ∈ f

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

source

theorem nhds_le_of_le {α : Type u} [topological_space α] {f : filter α} {a : α} {s : set α} :

a ∈ s → is_open s → filter.principal s ≤ f → nhds a ≤ f

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

source

theorem mem_nhds_sets_iff {α : Type u} [topological_space α] {a : α} {s : set α} :

s ∈ nhds a ↔ ∃ (t : set α) (H : t ⊆ s), is_open t ∧ a ∈ t

source

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

(∀ᶠ (x : α) in nhds a, p x) ↔ ∃ (t : set α), (∀ (x : α), x ∈ t → p x) ∧ is_open 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.

source

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

filter.map f (nhds a) = ⨅ (s : set α) (H : s ∈ {s : set α | a ∈ s ∧ is_open s}), filter.principal (f '' s)

source

theorem mem_of_nhds {α : Type u} [topological_space α] {a : α} {s : set α} :

s ∈ nhds a → a ∈ s

source

theorem filter.eventually.self_of_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} :

(∀ᶠ (y : α) in nhds a, p y) → p a

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

source

theorem mem_nhds_sets {α : Type u} [topological_space α] {a : α} {s : set α} :

is_open s → a ∈ s → s ∈ nhds a

source

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

(nhds a).has_basis (λ (s : set α), s ∈ nhds a ∧ is_open s) (λ (x : set α), 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.

source

theorem filter.eventually.eventually_nhds {α : Type u} [topological_space α] {p : α → Prop} {a : α} :

(∀ᶠ (y : α) in nhds a, p y) → (∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhds y, p x)

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

source

@[simp]

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

(∀ᶠ (y : α) in nhds a, ∀ᶠ (x : α) in nhds y, p x) ↔ ∀ᶠ (x : α) in nhds a, p x

source

@[simp]

theorem nhds_bind_nhds {α : Type u} {a : α} [topological_space α] :

(nhds a).bind nhds = nhds a

source

@[simp]

theorem eventually_eventually_eq_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} :

(∀ᶠ (y : α) in nhds a, f =ᶠ[nhds y] g) ↔ f =ᶠ[nhds a] g

source

theorem filter.eventually_eq.eq_of_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} :

f =ᶠ[nhds a] g → f a = g a

source

@[simp]

theorem eventually_eventually_le_nhds {α : Type u} {β : Type v} [topological_space α] [has_le β] {f g : α → β} {a : α} :

(∀ᶠ (y : α) in nhds a, f ≤ᶠ[nhds y] g) ↔ f ≤ᶠ[nhds a] g

source

theorem filter.eventually_eq.eventually_eq_nhds {α : Type u} {β : Type v} [topological_space α] {f g : α → β} {a : α} :

f =ᶠ[nhds a] g → (∀ᶠ (y : α) in nhds a, f =ᶠ[nhds y] g)

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

source

theorem filter.eventually_le.eventually_le_nhds {α : Type u} {β : Type v} [topological_space α] [has_le β] {f g : α → β} {a : α} :

f ≤ᶠ[nhds a] g → (∀ᶠ (y : α) in nhds a, f ≤ᶠ[nhds y] g)

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

source

theorem all_mem_nhds {α : Type u} [topological_space α] (x : α) (P : set α → Prop) :

(∀ (s t : set α), s ⊆ t → P s → P t) → ((∀ (s : set α), s ∈ nhds x → P s) ↔ ∀ (s : set α), is_open s → x ∈ s → P s)

source

theorem all_mem_nhds_filter {α : Type u} {β : Type v} [topological_space α] (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 α), is_open s → x ∈ s → f s ∈ l

source

theorem rtendsto_nhds {α : Type u} {β : Type v} [topological_space α] {r : rel β α} {l : filter β} {a : α} :

filter.rtendsto r l (nhds a) ↔ ∀ (s : set α), is_open s → a ∈ s → r.core s ∈ l

source

theorem rtendsto'_nhds {α : Type u} {β : Type v} [topological_space α] {r : rel β α} {l : filter β} {a : α} :

filter.rtendsto' r l (nhds a) ↔ ∀ (s : set α), is_open s → a ∈ s → r.preimage s ∈ l

source

theorem ptendsto_nhds {α : Type u} {β : Type v} [topological_space α] {f : β →. α} {l : filter β} {a : α} :

filter.ptendsto f l (nhds a) ↔ ∀ (s : set α), is_open s → a ∈ s → f.core s ∈ l

source

theorem ptendsto'_nhds {α : Type u} {β : Type v} [topological_space α] {f : β →. α} {l : filter β} {a : α} :

filter.ptendsto' f l (nhds a) ↔ ∀ (s : set α), is_open s → a ∈ s → f.preimage s ∈ l

source

theorem tendsto_nhds {α : Type u} {β : Type v} [topological_space α] {f : β → α} {l : filter β} {a : α} :

filter.tendsto f l (nhds a) ↔ ∀ (s : set α), is_open s → a ∈ s → f ⁻¹' s ∈ l

source

theorem tendsto_const_nhds {α : Type u} {β : Type v} [topological_space α] {a : α} {f : filter β} :

filter.tendsto (λ (b : β), a) f (nhds a)

source

theorem pure_le_nhds {α : Type u} [topological_space α] :

has_pure.pure ≤ nhds

source

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

filter.tendsto f (has_pure.pure a) (nhds (f a))

source

theorem order_top.tendsto_at_top_nhds {β : Type v} {α : Type u_1} [order_top α] [topological_space β] (f : α → β) :

filter.tendsto f filter.at_top (nhds (f ⊤))

source

@[simp, instance]

def nhds_ne_bot {α : Type u} [topological_space α] {a : α} :

(nhds a).ne_bot

Equations

nhds_ne_bot = _

source

def cluster_pt {α : Type u} [topological_space α] :

α → filter α → Prop

A point x is a cluster point of a filter F if 𝓝 x ⊓ F ≠ ⊥. Also known as an accumulation point or a limit point.

Equations

cluster_pt x F = (nhds x ⊓ F).ne_bot

source

theorem cluster_pt.ne_bot {α : Type u} [topological_space α] {x : α} {F : filter α} :

cluster_pt x F → (nhds x ⊓ F).ne_bot

source

theorem cluster_pt_iff {α : Type u} [topological_space α] {x : α} {F : filter α} :

cluster_pt x F ↔ ∀ {U V : set α}, U ∈ nhds x → V ∈ F → (U ∩ V).nonempty

source

theorem cluster_pt_principal_iff {α : Type u} [topological_space α] {x : α} {s : set α} :

cluster_pt x (filter.principal s) ↔ ∀ (U : set α), 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.

source

theorem cluster_pt_principal_iff_frequently {α : Type u} [topological_space α] {x : α} {s : set α} :

cluster_pt x (filter.principal s) ↔ ∃ᶠ (y : α) in nhds x, y ∈ s

source

theorem cluster_pt.of_le_nhds {α : Type u} [topological_space α] {x : α} {f : filter α} (H : f ≤ nhds x) [f.ne_bot] :

cluster_pt x f

source

theorem cluster_pt.of_le_nhds' {α : Type u} [topological_space α] {x : α} {f : filter α} :

f ≤ nhds x → f.ne_bot → cluster_pt x f

source

theorem cluster_pt.of_nhds_le {α : Type u} [topological_space α] {x : α} {f : filter α} :

nhds x ≤ f → cluster_pt x f

source

theorem cluster_pt.mono {α : Type u} [topological_space α] {x : α} {f g : filter α} :

cluster_pt x f → f ≤ g → cluster_pt x g

source

theorem cluster_pt.of_inf_left {α : Type u} [topological_space α] {x : α} {f g : filter α} :

cluster_pt x (f ⊓ g) → cluster_pt x f

source

theorem cluster_pt.of_inf_right {α : Type u} [topological_space α] {x : α} {f g : filter α} :

cluster_pt x (f ⊓ g) → cluster_pt x g

source

def map_cluster_pt {α : Type u} [topological_space α] {ι : Type u_1} :

α → filter ι → (ι → α) → Prop

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

Equations

map_cluster_pt x F u = cluster_pt x (filter.map u F)

source

theorem map_cluster_pt_iff {α : Type u} [topological_space α] {ι : Type u_1} (x : α) (F : filter ι) (u : ι → α) :

map_cluster_pt x F u ↔ ∀ (s : set α), s ∈ nhds x → (∃ᶠ (a : ι) in F, u a ∈ s)

source

theorem map_cluster_pt_of_comp {α : Type u} [topological_space α] {ι : Type u_1} {δ : Type u_2} {F : filter ι} {φ : δ → ι} {p : filter δ} {x : α} {u : ι → α} [p.ne_bot] :

filter.tendsto φ p F → filter.tendsto (u ∘ φ) p (nhds x) → map_cluster_pt x F u

source

theorem interior_eq_nhds {α : Type u} [topological_space α] {s : set α} :

interior s = {a : α | nhds a ≤ filter.principal s}

source

theorem mem_interior_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :

a ∈ interior s ↔ s ∈ nhds a

source

theorem subset_interior_iff_nhds {α : Type u} [topological_space α] {s V : set α} :

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

source

theorem is_open_iff_nhds {α : Type u} [topological_space α] {s : set α} :

is_open s ↔ ∀ (a : α), a ∈ s → nhds a ≤ filter.principal s

source

theorem is_open_iff_mem_nhds {α : Type u} [topological_space α] {s : set α} :

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

source

theorem mem_closure_iff_frequently {α : Type u} [topological_space α] {s : set α} {a : α} :

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

source

theorem mem_closure_iff_cluster_pt {α : Type u} [topological_space α] {s : set α} {a : α} :

a ∈ closure s ↔ cluster_pt a (filter.principal s)

source

theorem closure_eq_cluster_pts {α : Type u} [topological_space α] {s : set α} :

closure s = {a : α | cluster_pt a (filter.principal s)}

source

theorem mem_closure_iff_nhds {α : Type u} [topological_space α] {s : set α} {a : α} :

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

source

theorem mem_closure_iff_nhds' {α : Type u} [topological_space α] {s : set α} {a : α} :

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

source

theorem mem_closure_iff_comap_ne_bot {α : Type u} [topological_space α] {A : set α} {x : α} :

x ∈ closure A ↔ (filter.comap coe (nhds x)).ne_bot

source

theorem mem_closure_iff_nhds_basis {α : Type u} {β : Type v} [topological_space α] {a : α} {p : β → Prop} {s : β → set α} (h : (nhds a).has_basis p s) {t : set α} :

a ∈ closure t ↔ ∀ (i : β), p i → (∃ (y : α) (H : y ∈ t), y ∈ s i)

source

theorem mem_closure_iff_ultrafilter {α : Type u} [topological_space α] {s : set α} {x : α} :

x ∈ closure s ↔ ∃ (u : filter.ultrafilter α), s ∈ u.val ∧ u.val ≤ nhds x

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

source

theorem is_closed_iff_cluster_pt {α : Type u} [topological_space α] {s : set α} :

is_closed s ↔ ∀ (a : α), cluster_pt a (filter.principal s) → a ∈ s

source

theorem is_closed_iff_nhds {α : Type u} [topological_space α] {s : set α} :

is_closed s ↔ ∀ (x : α), (∀ (U : set α), U ∈ nhds x → (U ∩ s).nonempty) → x ∈ s

source

theorem closure_inter_open {α : Type u} [topological_space α] {s t : set α} :

is_open s → s ∩ closure t ⊆ closure (s ∩ t)

source

theorem dense_inter_of_open_left {α : Type u} [topological_space α] {s t : set α} :

closure s = set.univ → closure t = set.univ → is_open s → closure (s ∩ t) = set.univ

source

theorem dense_inter_of_open_right {α : Type u} [topological_space α] {s t : set α} :

closure s = set.univ → closure t = set.univ → is_open t → closure (s ∩ t) = set.univ

source

theorem closure_diff {α : Type u} [topological_space α] {s t : set α} :

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

source

theorem filter.frequently.mem_of_closed {α : Type u} [topological_space α] {a : α} {s : set α} :

(∃ᶠ (x : α) in nhds a, x ∈ s) → is_closed s → a ∈ s

source

theorem is_closed.mem_of_frequently_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} :

is_closed s → (∃ᶠ (x : β) in b, f x ∈ s) → filter.tendsto f b (nhds a) → a ∈ s

source

theorem is_closed.mem_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} [b.ne_bot] :

is_closed s → filter.tendsto f b (nhds a) → (∀ᶠ (x : β) in b, f x ∈ s) → a ∈ s

source

theorem mem_closure_of_tendsto {α : Type u} {β : Type v} [topological_space α] {f : β → α} {b : filter β} {a : α} {s : set α} [b.ne_bot] :

filter.tendsto f b (nhds a) → (∀ᶠ (x : β) in b, f x ∈ s) → a ∈ closure s

source

theorem tendsto_inf_principal_nhds_iff_of_forall_eq {α : Type u} {β : Type v} [topological_space α] {f : β → α} {l : filter β} {s : set β} {a : α} :

(∀ (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.

source

def Lim {α : Type u} [topological_space α] [nonempty α] :

filter α → α

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

Equations

Lim f = classical.epsilon (λ (a : α), f ≤ nhds a)

source

def lim {α : Type u} {β : Type v} [topological_space α] [nonempty α] :

filter β → (β → α) → α

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

Equations

lim f g = Lim (filter.map g f)

source

theorem Lim_spec {α : Type u} [topological_space α] {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 𝓝 (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.

source

theorem lim_spec {α : Type u} {β : Type v} [topological_space α] {f : filter β} {g : β → α} (h : ∃ (a : α), filter.tendsto g f (nhds a)) :

filter.tendsto g f (nhds (lim f g))

If g tends to some 𝓝 a along f, then it tends to 𝓝 (lim 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.

source

def locally_finite {α : Type u} {β : Type v} [topological_space α] :

(β → set α) → Prop

A family of sets in set α is locally finite if at every point x:α, there is a neighborhood of x which meets only finitely many sets in the family

Equations

locally_finite f = ∀ (x : α), ∃ (t : set α) (H : t ∈ nhds x), {i : β | (f i ∩ t).nonempty}.finite

source

theorem locally_finite_of_finite {α : Type u} {β : Type v} [topological_space α] {f : β → set α} :

set.univ.finite → locally_finite f

source

theorem locally_finite_subset {α : Type u} {β : Type v} [topological_space α] {f₁ f₂ : β → set α} :

locally_finite f₂ → (∀ (b : β), f₁ b ⊆ f₂ b) → locally_finite f₁

source

theorem is_closed_Union_of_locally_finite {α : Type u} {β : Type v} [topological_space α] {f : β → set α} :

locally_finite f → (∀ (i : β), is_closed (f i)) → is_closed (⋃ (i : β), f i)

source

def continuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

(α → β) → Prop

A function between topological spaces is continuous if the preimage of every open set is open.

Equations

continuous f = ∀ (s : set β), is_open s → is_open (f ⁻¹' s)

source

theorem is_open.preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set β} :

is_open s → is_open (f ⁻¹' s)

source

def continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

(α → β) → α → Prop

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

Equations

continuous_at f x = filter.tendsto f (nhds x) (nhds (f x))

source

theorem continuous_at.tendsto {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} :

continuous_at f x → filter.tendsto f (nhds x) (nhds (f x))

source

theorem continuous_at.preimage_mem_nhds {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} {t : set β} :

continuous_at f x → t ∈ nhds (f x) → f ⁻¹' t ∈ nhds x

source

theorem preimage_interior_subset_interior_preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set β} :

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

source

theorem continuous_id {α : Type u_1} [topological_space α] :

continuous id

source

theorem continuous.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} :

continuous g → continuous f → continuous (g ∘ f)

source

theorem continuous.iterate {α : Type u_1} [topological_space α] {f : α → α} (h : continuous f) (n : ℕ) :

continuous f^[n]

source

theorem continuous_at.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [topological_space α] [topological_space β] [topological_space γ] {g : β → γ} {f : α → β} {x : α} :

continuous_at g (f x) → continuous_at f x → continuous_at (g ∘ f) x

source

theorem continuous.tendsto {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) (x : α) :

filter.tendsto f (nhds x) (nhds (f x))

source

theorem continuous.continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {x : α} :

continuous f → continuous_at f x

source

theorem continuous_iff_continuous_at {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :

continuous f ↔ ∀ (x : α), continuous_at f x

source

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

continuous (λ (a : α), b)

source

theorem continuous_at_const {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {x : α} {b : β} :

continuous_at (λ (a : α), b) x

source

theorem continuous_at_id {α : Type u_1} [topological_space α] {x : α} :

continuous_at id x

source

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

continuous_at f^[n] x

source

theorem continuous_iff_is_closed {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} :

continuous f ↔ ∀ (s : set β), is_closed s → is_closed (f ⁻¹' s)

source

theorem is_closed.preimage {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (hf : continuous f) {s : set β} :

is_closed s → is_closed (f ⁻¹' s)

source

theorem continuous_at_iff_ultrafilter {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} (x : α) :

continuous_at f x ↔ ∀ (g : filter α), g.is_ultrafilter → g ≤ nhds x → filter.map f g ≤ nhds (f x)

source

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

continuous f ↔ ∀ (x : α) (g : filter α), g.is_ultrafilter → g ≤ nhds x → filter.map f g ≤ nhds (f x)

source

theorem continuous_if {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {p : α → Prop} {f g : α → β} {h : Π (a : α), decidable (p a)} :

(∀ (a : α), a ∈ frontier {a : α | p a} → f a = g a) → continuous f → continuous g → continuous (λ (a : α), ite (p a) (f a) (g a))

A piecewise defined function if p then f else g is continuous, if both f and g are continuous, and they coincide on the frontier (boundary) of the set {a | p a}.

source

def pcontinuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] :

(α →. β) → Prop

Continuity of a partial function

Equations

pcontinuous f = ∀ (s : set β), is_open s → is_open (f.preimage s)

source

theorem open_dom_of_pcontinuous {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} :

pcontinuous f → is_open f.dom

source

theorem pcontinuous_iff' {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α →. β} :

pcontinuous f ↔ ∀ {x : α} {y : β}, y ∈ f x → filter.ptendsto' f (nhds x) (nhds y)

source

theorem image_closure_subset_closure_image {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {f : α → β} {s : set α} :

continuous f → f '' closure s ⊆ closure (f '' s)

source

theorem mem_closure {α : Type u_1} {β : Type u_2} [topological_space α] [topological_space β] {s : set α} {t : set β} {f : α → β} {a : α} :

continuous f → a ∈ closure s → (∀ (a : α), a ∈ s → f a ∈ t) → f a ∈ closure t

mathlib documentation

topology.basic

Basic theory of topological spaces.

Notation

Implementation notes

References

Tags

Topological spaces

Interior of a set

Closure of a set

Frontier of a set

Neighborhoods

Cluster points

Interior, closure and frontier in terms of neighborhoods

Limits of filters in topological spaces

Locally finite families

Continuity

General documentation

Additional documentation

Library

mathlib documentation

topology.​basic

Basic theory of topological spaces.

Notation

Implementation notes

References

Tags

Topological spaces

Interior of a set

Closure of a set

Frontier of a set

Neighborhoods

Cluster points

Interior, closure and frontier in terms of neighborhoods

Limits of filters in topological spaces

Locally finite families

Continuity

General documentation

Additional documentation

Library

topology.basic