mathlib documentation

topology.constructions

Constructions of new topological spaces from old ones

This file constructs products, sums, subtypes and quotients of topological spaces and sets up their basic theory, such as criteria for maps into or out of these constructions to be continuous; descriptions of the open sets, neighborhood filters, and generators of these constructions; and their behavior with respect to embeddings and other specific classes of maps.

Implementation note

The constructed topologies are defined using induced and coinduced topologies along with the complete lattice structure on topologies. Their universal properties (for example, a map X → Y × Z is continuous if and only if both projections X → Y, X → Z are) follow easily using order-theoretic descriptions of continuity. With more work we can also extract descriptions of the open sets, neighborhood filters and so on.

Tags

product, sum, disjoint union, subspace, quotient space

@[instance]
def subtype.topological_space {α : Type u} {p : α → Prop} [t : topological_space α] :

Equations
@[instance]
def quot.topological_space {α : Type u} {r : α → α → Prop} [t : topological_space α] :

Equations
@[instance]
def sigma.topological_space {α : Type u} {β : α → Type v} [t₂ : Π (a : α), topological_space (β a)] :

Equations
@[instance]
def Pi.topological_space {α : Type u} {β : α → Type v} [t₂ : Π (a : α), topological_space (β a)] :
topological_space (Π (a : α), β a)

Equations
theorem dense.quotient {α : Type u} [setoid α] [topological_space α] {s : set α} :

The image of a dense set under quotient.mk is a dense set.

theorem dense_range.quotient {α : Type u} {β : Type v} [setoid α] [topological_space α] {f : β → α} :

The composition of quotient.mk and a function with dense range has dense range.

@[instance]
def subtype.discrete_topology {α : Type u} {p : α → Prop} [topological_space α] [discrete_topology α] :

@[instance]
def sum.discrete_topology {α : Type u} {β : Type v} [topological_space α] [topological_space β] [hα : discrete_topology α] [hβ : discrete_topology β] :

@[instance]
def sigma.discrete_topology {α : Type u} {β : α → Type v} [Π (a : α), topological_space (β a)] [h : ∀ (a : α), discrete_topology (β a)] :

theorem mem_nhds_subtype {α : Type u} [topological_space α] (s : set α) (a : {x // x s}) (t : set {x // x s}) :
t 𝓝 a ∃ (u : set α) (H : u 𝓝 a), coe ⁻¹' u t

theorem nhds_subtype {α : Type u} [topological_space α] (s : set α) (a : {x // x s}) :

theorem continuous_fst {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

theorem continuous_at_fst {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α × β} :

theorem continuous_snd {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

theorem continuous_at_snd {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α × β} :

theorem continuous.prod_mk {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [topological_space β] [topological_space γ] {f : γ → α} {g : γ → β} :
continuous fcontinuous gcontinuous (λ (x : γ), (f x, g x))

theorem continuous.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : γ → α} {g : δ → β} :
continuous fcontinuous gcontinuous (λ (x : γ × δ), (f x.fst, g x.snd))

theorem filter.eventually.prod_inl_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α → Prop} {a : α} (h : ∀ᶠ (x : α) in 𝓝 a, p x) (b : β) :
∀ᶠ (x : α × β) in 𝓝 (a, b), p x.fst

theorem filter.eventually.prod_inr_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : β → Prop} {b : β} (h : ∀ᶠ (x : β) in 𝓝 b, p x) (a : α) :
∀ᶠ (x : α × β) in 𝓝 (a, b), p x.snd

theorem filter.eventually.prod_mk_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] {pa : α → Prop} {a : α} (ha : ∀ᶠ (x : α) in 𝓝 a, pa x) {pb : β → Prop} {b : β} :
(∀ᶠ (y : β) in 𝓝 b, pb y)(∀ᶠ (p : α × β) in 𝓝 (a, b), pa p.fst pb p.snd)

theorem continuous_swap {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

theorem is_open.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :
is_open sis_open tis_open (s.prod t)

theorem nhds_prod_eq {α : Type u} {β : Type v} [topological_space α] [topological_space β] {a : α} {b : β} :
𝓝 (a, b) = 𝓝 a ×ᶠ 𝓝 b

theorem mem_nhds_prod_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] {a : α} {b : β} {s : set × β)} :
s 𝓝 (a, b) ∃ (u : set α) (H : u 𝓝 a) (v : set β) (H : v 𝓝 b), u.prod v s

theorem filter.has_basis.prod_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] {ιa : Type u_1} {ιb : Type u_2} {pa : ιa → Prop} {pb : ιb → Prop} {sa : ιa → set α} {sb : ιb → set β} {a : α} {b : β} :
(𝓝 a).has_basis pa sa(𝓝 b).has_basis pb sb(𝓝 (a, b)).has_basis (λ (i : ιa × ιb), pa i.fst pb i.snd) (λ (i : ιa × ιb), (sa i.fst).prod (sb i.snd))

@[instance]

theorem prod_mem_nhds_sets {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} {a : α} {b : β} :
s 𝓝 at 𝓝 bs.prod t 𝓝 (a, b)

theorem nhds_swap {α : Type u} {β : Type v} [topological_space α] [topological_space β] (a : α) (b : β) :
𝓝 (a, b) = filter.map prod.swap (𝓝 (b, a))

theorem filter.tendsto.prod_mk_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] {γ : Type u_1} {a : α} {b : β} {f : filter γ} {ma : γ → α} {mb : γ → β} :
filter.tendsto ma f (𝓝 a)filter.tendsto mb f (𝓝 b)filter.tendsto (λ (c : γ), (ma c, mb c)) f (𝓝 (a, b))

theorem filter.eventually.curry_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α × β → Prop} {x : α} {y : β} :
(∀ᶠ (x : α × β) in 𝓝 (x, y), p x)(∀ᶠ (x' : α) in 𝓝 x, ∀ᶠ (y' : β) in 𝓝 y, p (x', y'))

theorem continuous_at.prod {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [topological_space β] [topological_space γ] {f : α → β} {g : α → γ} {x : α} :
continuous_at f xcontinuous_at g xcontinuous_at (λ (x : α), (f x, g x)) x

theorem continuous_at.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α → γ} {g : β → δ} {p : α × β} :
continuous_at f p.fstcontinuous_at g p.sndcontinuous_at (λ (p : α × β), (f p.fst, g p.snd)) p

theorem continuous_at.prod_map' {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α → γ} {g : β → δ} {x : α} {y : β} :
continuous_at f xcontinuous_at g ycontinuous_at (λ (p : α × β), (f p.fst, g p.snd)) (x, y)

theorem prod_generate_from_generate_from_eq {α : Type u_1} {β : Type u_2} {s : set (set α)} {t : set (set β)} :
⋃₀s = set.univ⋃₀t = set.univprod.topological_space = topological_space.generate_from {g : set × β) | ∃ (u : set α) (H : u s) (v : set β) (H : v t), g = u.prod v}

theorem prod_eq_generate_from {α : Type u} {β : Type v} [topological_space α] [topological_space β] :
prod.topological_space = topological_space.generate_from {g : set × β) | ∃ (s : set α) (t : set β), is_open s is_open t g = s.prod t}

theorem is_open_prod_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set × β)} :
is_open s ∀ (a : α) (b : β), (a, b) s(∃ (u : set α) (v : set β), is_open u is_open v a u b v u.prod v s)

theorem exists_nhds_square {α : Type u} [topological_space α] {s : set × α)} {x : α} :
s 𝓝 (x, x)(∃ (U : set α), is_open U x U U.prod U s)

Given a neighborhood s of (x, x), then (x, x) has a square open neighborhood that is a subset of s.

theorem is_open_map_fst {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

The first projection in a product of topological spaces sends open sets to open sets.

theorem is_open_map_snd {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

The second projection in a product of topological spaces sends open sets to open sets.

theorem is_open_prod_iff' {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :

A product set is open in a product space if and only if each factor is open, or one of them is empty

theorem closure_prod_eq {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :

theorem mem_closure2 {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [topological_space β] [topological_space γ] {s : set α} {t : set β} {u : set γ} {f : α → β → γ} {a : α} {b : β} :
continuous (λ (p : α × β), f p.fst p.snd)a closure sb closure t(∀ (a : α) (b : β), a sb tf a b u)f a b closure u

theorem is_closed.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s₁ : set α} {s₂ : set β} :
is_closed s₁is_closed s₂is_closed (s₁.prod s₂)

theorem dense.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} :
dense sdense tdense (s.prod t)

The product of two dense sets is a dense set.

theorem dense_range.prod_map {β : Type v} {γ : Type w} [topological_space β] [topological_space γ] {ι : Type u_1} {κ : Type u_2} {f : ι → β} {g : κ → γ} :

If f and g are maps with dense range, then prod.map f g has dense range.

theorem inducing.prod_mk {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α → β} {g : γ → δ} :
inducing finducing ginducing (λ (x : α × γ), (f x.fst, g x.snd))

theorem embedding.prod_mk {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α → β} {g : γ → δ} :
embedding fembedding gembedding (λ (x : α × γ), (f x.fst, g x.snd))

theorem is_open_map.prod {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α → β} {g : γ → δ} :
is_open_map fis_open_map gis_open_map (λ (p : α × γ), (f p.fst, g p.snd))

theorem open_embedding.prod {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α → β} {g : γ → δ} :
open_embedding fopen_embedding gopen_embedding (λ (x : α × γ), (f x.fst, g x.snd))

theorem embedding_graph {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} :
continuous fembedding (λ (x : α), (x, f x))

theorem continuous_inl {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

theorem continuous_inr {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

theorem continuous_sum_rec {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [topological_space β] [topological_space γ] {f : α → γ} {g : β → γ} :
continuous fcontinuous gcontinuous (sum.rec f g)

theorem is_open_sum_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set β)} :

theorem is_open_map_sum {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [topological_space β] [topological_space γ] {f : α β → γ} :
is_open_map (λ (a : α), f (sum.inl a))is_open_map (λ (b : β), f (sum.inr b))is_open_map f

theorem embedding_inl {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

theorem embedding_inr {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

theorem open_embedding_inl {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

theorem open_embedding_inr {α : Type u} {β : Type v} [topological_space α] [topological_space β] :

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

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

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

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

theorem is_open_map.restrict {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} (hf : is_open_map f) {s : set α} :

theorem continuous_subtype_mk {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α → Prop} {f : β → α} (hp : ∀ (x : β), p (f x)) :
continuous fcontinuous (λ (x : β), f x, _⟩)

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

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

theorem map_nhds_subtype_coe_eq {α : Type u} [topological_space α] {p : α → Prop} {a : α} (ha : p a) :
{a : α | p a} 𝓝 afilter.map coe (𝓝 a, ha⟩) = 𝓝 a

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

theorem tendsto_subtype_rng {α : Type u} [topological_space α] {β : Type u_1} {p : α → Prop} {b : filter β} {f : β → subtype p} {a : subtype p} :
filter.tendsto f b (𝓝 a) filter.tendsto (λ (x : β), (f x)) b (𝓝 a)

theorem continuous_subtype_nhds_cover {α : Type u} {β : Type v} [topological_space α] [topological_space β] {ι : Sort u_1} {f : α → β} {c : ι → α → Prop} :
(∀ (x : α), ∃ (i : ι), {x : α | c i x} 𝓝 x)(∀ (i : ι), continuous (λ (x : subtype (c i)), f x))continuous f

theorem continuous_subtype_is_closed_cover {α : Type u} {β : Type v} [topological_space α] [topological_space β] {ι : Type u_1} {f : α → β} (c : ι → α → Prop) :
locally_finite (λ (i : ι), {x : α | c i x})(∀ (i : ι), is_closed {x : α | c i x})(∀ (x : α), ∃ (i : ι), c i x)(∀ (i : ι), continuous (λ (x : subtype (c i)), f x))continuous f

theorem closure_subtype {α : Type u} [topological_space α] {p : α → Prop} {x : {a // p a}} {s : set {a // p a}} :

theorem quotient_map_quot_mk {α : Type u} [topological_space α] {r : α → α → Prop} :
quotient_map (quot.mk r)

theorem continuous_quot_mk {α : Type u} [topological_space α] {r : α → α → Prop} :
continuous (quot.mk r)

theorem continuous_quot_lift {α : Type u} {β : Type v} [topological_space α] [topological_space β] {r : α → α → Prop} {f : α → β} (hr : ∀ (a b : α), r a bf a = f b) :
continuous fcontinuous (quot.lift f hr)

theorem continuous_quotient_lift {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : setoid α} {f : α → β} (hs : ∀ (a b : α), a bf a = f b) :

theorem continuous_pi {α : Type u} {ι : Type u_1} {π : ι → Type u_2} [topological_space α] [Π (i : ι), topological_space («π» i)] {f : α → Π (i : ι), «π» i} :
(∀ (i : ι), continuous (λ (a : α), f a i))continuous f

theorem continuous_apply {ι : Type u_1} {π : ι → Type u_2} [Π (i : ι), topological_space («π» i)] (i : ι) :
continuous (λ (p : Π (i : ι), «π» i), p i)

theorem continuous_update {ι : Type u_1} {π : ι → Type u_2} [decidable_eq ι] [Π (i : ι), topological_space («π» i)] {i : ι} {f : Π (i : ι), «π» i} :
continuous (λ (x : «π» i), function.update f i x)

Embedding a factor into a product space (by fixing arbitrarily all the other coordinates) is continuous.

theorem nhds_pi {ι : Type u_1} {π : ι → Type u_2} [t : Π (i : ι), topological_space («π» i)] {a : Π (i : ι), «π» i} :
𝓝 a = ⨅ (i : ι), filter.comap (λ (x : Π (i : ι), «π» i), x i) (𝓝 (a i))

theorem tendsto_pi {α : Type u} {ι : Type u_1} {π : ι → Type u_2} [t : Π (i : ι), topological_space («π» i)] {f : α → Π (i : ι), «π» i} {g : Π (i : ι), «π» i} {u : filter α} :
filter.tendsto f u (𝓝 g) ∀ (x : ι), filter.tendsto (λ (i : α), f i x) u (𝓝 (g x))

theorem is_open_set_pi {ι : Type u_1} {π : ι → Type u_2} [Π (a : ι), topological_space («π» a)] {i : set ι} {s : Π (a : ι), set («π» a)} :
i.finite(∀ (a : ι), a iis_open (s a))is_open (i.pi s)

theorem pi_eq_generate_from {ι : Type u_1} {π : ι → Type u_2} [Π (a : ι), topological_space («π» a)] :
Pi.topological_space = topological_space.generate_from {g : set (Π (a : ι), «π» a) | ∃ (s : Π (a : ι), set («π» a)) (i : finset ι), (∀ (a : ι), a iis_open (s a)) g = i.pi s}

theorem pi_generate_from_eq {ι : Type u_1} {π : ι → Type u_2} {g : Π (a : ι), set (set («π» a))} :
Pi.topological_space = topological_space.generate_from {t : set (Π (a : ι), «π» a) | ∃ (s : Π (a : ι), set («π» a)) (i : finset ι), (∀ (a : ι), a is a g a) t = i.pi s}

theorem pi_generate_from_eq_fintype {ι : Type u_1} {π : ι → Type u_2} {g : Π (a : ι), set (set («π» a))} [fintype ι] :
(∀ (a : ι), ⋃₀g a = set.univ)Pi.topological_space = topological_space.generate_from {t : set (Π (a : ι), «π» a) | ∃ (s : Π (a : ι), set («π» a)), (∀ (a : ι), s a g a) t = set.univ.pi s}

theorem continuous_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

theorem is_open_sigma_iff {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {s : set (sigma σ)} :
is_open s ∀ (i : ι), is_open (sigma.mk i ⁻¹' s)

theorem is_closed_sigma_iff {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {s : set (sigma σ)} :
is_closed s ∀ (i : ι), is_closed (sigma.mk i ⁻¹' s)

theorem is_open_map_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

theorem is_open_range_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

theorem is_closed_map_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

theorem is_closed_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

theorem open_embedding_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

theorem closed_embedding_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

theorem embedding_sigma_mk {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {i : ι} :

theorem continuous_sigma {β : Type v} {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] [topological_space β] {f : sigma σ → β} :
(∀ (i : ι), continuous (λ (a : σ i), f i, a⟩))continuous f

A map out of a sum type is continuous if its restriction to each summand is.

theorem continuous_sigma_map {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {κ : Type u_3} {τ : κ → Type u_4} [Π (k : κ), topological_space (τ k)] {f₁ : ι → κ} {f₂ : Π (i : ι), σ iτ (f₁ i)} :
(∀ (i : ι), continuous (f₂ i))continuous (sigma.map f₁ f₂)

theorem is_open_map_sigma {β : Type v} {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] [topological_space β] {f : sigma σ → β} :
(∀ (i : ι), is_open_map (λ (a : σ i), f i, a⟩))is_open_map f

theorem embedding_sigma_map {ι : Type u_1} {σ : ι → Type u_2} [Π (i : ι), topological_space (σ i)] {τ : ι → Type u_3} [Π (i : ι), topological_space (τ i)] {f : Π (i : ι), σ iτ i} :
(∀ (i : ι), embedding (f i))embedding (sigma.map id f)

The sum of embeddings is an embedding.

theorem continuous_ulift_up {α : Type u} [topological_space α] :
continuous ulift.up

theorem mem_closure_of_continuous {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α → β} {a : α} {s : set α} {t : set β} :
continuous fa closure sset.maps_to f s (closure t)f a closure t

theorem mem_closure_of_continuous2 {α : Type u} {β : Type v} {γ : Type w} [topological_space α] [topological_space β] [topological_space γ] {f : α → β → γ} {a : α} {b : β} {s : set α} {t : set β} {u : set γ} :
continuous (λ (p : α × β), f p.fst p.snd)a closure sb closure t(∀ (a : α), a s∀ (b : β), b tf a b closure u)f a b closure u