# mathlibdocumentation

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 quotient.topological_space {α : Type u} {s : setoid α} [t : topological_space α] :

Equations
@[instance]
def prod.topological_space {α : Type u} {β : Type v} [t₁ : topological_space α] [t₂ : topological_space β] :

Equations
@[instance]
def sum.topological_space {α : Type u} {β : Type v} [t₁ : topological_space α] [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
@[instance]
def ulift.topological_space {α : Type u} [t : topological_space α] :

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

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

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

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

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

@[instance]
def sum.discrete_topology {α : Type u} {β : Type v} [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} (s : set α) (a : {x // x s}) (t : set {x // x s}) :
t 𝓝 a ∃ (u : set α) (H : u 𝓝 a), t

theorem nhds_subtype {α : Type u} (s : set α) (a : {x // x s}) :
𝓝 a = (𝓝 a)

theorem continuous_fst {α : Type u} {β : Type v}  :

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

theorem continuous_snd {α : Type u} {β : Type v}  :

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

theorem continuous.prod_mk {α : Type u} {β : Type v} {γ : Type w} {f : γ → α} {g : γ → β} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : γ), (f x, g x))

theorem continuous.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {f : γ → α} {g : δ → β} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : γ × δ), (f x.fst, g x.snd))

theorem filter.eventually.prod_inl_nhds {α : Type u} {β : Type v} {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} {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} {pa : α → Prop} {a : α} (ha : ∀ᶠ (x : α) in 𝓝 a, pa x) {pb : β → Prop} {b : β} (hb : ∀ᶠ (y : β) in 𝓝 b, pb y) :
∀ᶠ (p : α × β) in 𝓝 (a, b), pa p.fst pb p.snd

theorem continuous_swap {α : Type u} {β : Type v}  :

theorem continuous_uncurry_left {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} (a : α) (h : continuous ) :

theorem continuous_uncurry_right {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} (b : β) (h : continuous ) :
continuous (λ (a : α), f a b)

theorem continuous_curry {α : Type u} {β : Type v} {γ : Type w} {g : α × β → γ} (a : α) (h : continuous g) :

theorem is_open.prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :

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

theorem mem_nhds_prod_iff {α : Type u} {β : Type v} {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} {ιa : Type u_1} {ιb : Type u_2} {pa : ιa → Prop} {pb : ιb → Prop} {sa : ιa → set α} {sb : ιb → set β} {a : α} {b : β} (ha : (𝓝 a).has_basis pa sa) (hb : (𝓝 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]
def prod.discrete_topology {α : Type u} {β : Type v}  :

theorem prod_mem_nhds_sets {α : Type u} {β : Type v} {s : set α} {t : set β} {a : α} {b : β} (ha : s 𝓝 a) (hb : t 𝓝 b) :
s.prod t 𝓝 (a, b)

theorem nhds_swap {α : Type u} {β : Type v} (a : α) (b : β) :
𝓝 (a, b) = (𝓝 (b, a))

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

theorem filter.eventually.curry_nhds {α : Type u} {β : Type v} {p : α × β → Prop} {x : α} {y : β} (h : ∀ᶠ (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} {f : α → β} {g : α → γ} {x : α} (hf : x) (hg : x) :
continuous_at (λ (x : α), (f x, g x)) x

theorem continuous_at.prod_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {f : α → γ} {g : β → δ} {p : α × β} (hf : p.fst) (hg : p.snd) :
continuous_at (λ (p : α × β), (f p.fst, g p.snd)) p

theorem continuous_at.prod_map' {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {f : α → γ} {g : β → δ} {x : α} {y : β} (hf : x) (hg : y) :
continuous_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 β)} (hs : ⋃₀s = set.univ) (ht : ⋃₀t = set.univ) :
prod.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}  :
prod.topological_space = topological_space.generate_from {g : set × β) | ∃ (s : set α) (t : set β), g = s.prod t}

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

theorem continuous_uncurry_of_discrete_topology_left {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} (h : ∀ (a : α), continuous (f a)) :

theorem exists_nhds_square {α : Type u} {s : set × α)} {x : α} (hx : s 𝓝 (x, x)) :
∃ (U : set α), 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}  :

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

theorem is_open_map_snd {α : Type u} {β : Type v}  :

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

theorem is_open_prod_iff' {α : Type u} {β : Type v} {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} {s : set α} {t : set β} :

theorem map_mem_closure2 {α : Type u} {β : Type v} {γ : Type w} {s : set α} {t : set β} {u : set γ} {f : α → β → γ} {a : α} {b : β} (hf : continuous (λ (p : α × β), f p.fst p.snd)) (ha : a ) (hb : b ) (hu : ∀ (a : α) (b : β), a sb tf a b u) :
f a b

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

theorem dense.prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : dense s) (ht : dense t) :
dense (s.prod t)

The product of two dense sets is a dense set.

theorem dense_range.prod_map {β : Type v} {γ : Type w} {ι : Type u_1} {κ : Type u_2} {f : ι → β} {g : κ → γ} (hf : dense_range f) (hg : dense_range 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} {f : α → β} {g : γ → δ} (hf : inducing f) (hg : inducing g) :
inducing (λ (x : α × γ), (f x.fst, g x.snd))

theorem embedding.prod_mk {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {f : α → β} {g : γ → δ} (hf : embedding f) (hg : embedding g) :
embedding (λ (x : α × γ), (f x.fst, g x.snd))

theorem is_open_map.prod {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {f : α → β} {g : γ → δ} (hf : is_open_map f) (hg : is_open_map g) :
is_open_map (λ (p : α × γ), (f p.fst, g p.snd))

theorem open_embedding.prod {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} {f : α → β} {g : γ → δ} (hf : open_embedding f) (hg : open_embedding g) :
open_embedding (λ (x : α × γ), (f x.fst, g x.snd))

theorem embedding_graph {α : Type u} {β : Type v} {f : α → β} (hf : continuous f) :
embedding (λ (x : α), (x, f x))

theorem continuous_inl {α : Type u} {β : Type v}  :

theorem continuous_inr {α : Type u} {β : Type v}  :

theorem continuous_sum_rec {α : Type u} {β : Type v} {γ : Type w} {f : α → γ} {g : β → γ} (hf : continuous f) (hg : continuous g) :
continuous (sum.rec f g)

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

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

theorem embedding_inl {α : Type u} {β : Type v}  :

theorem embedding_inr {α : Type u} {β : Type v}  :

theorem is_open_range_inl {α : Type u} {β : Type v}  :

theorem is_open_range_inr {α : Type u} {β : Type v}  :

theorem open_embedding_inl {α : Type u} {β : Type v}  :

theorem open_embedding_inr {α : Type u} {β : Type v}  :

theorem embedding_subtype_coe {α : Type u} {p : α → Prop} :

theorem continuous_subtype_val {α : Type u} {p : α → Prop} :

theorem continuous_subtype_coe {α : Type u} {p : α → Prop} :

theorem is_open.open_embedding_subtype_coe {α : Type u} {s : set α} (hs : is_open s) :

theorem is_open.is_open_map_subtype_coe {α : Type u} {s : set α} (hs : is_open s) :

theorem is_open_map.restrict {α : Type u} {β : Type v} {f : α → β} (hf : is_open_map f) {s : set α} (hs : is_open s) :

theorem is_closed.closed_embedding_subtype_coe {α : Type u} {s : set α} (hs : is_closed s) :

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

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

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

theorem map_nhds_subtype_coe_eq {α : Type u} {p : α → Prop} {a : α} (ha : p a) (h : {a : α | p a} 𝓝 a) :
(𝓝 a, ha⟩) = 𝓝 a

theorem nhds_subtype_eq_comap {α : Type u} {p : α → Prop} {a : α} {h : p a} :
𝓝 a, h⟩ = (𝓝 a)

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

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

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

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

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

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

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

theorem quotient_map_quotient_mk {α : Type u} {s : setoid α} :

theorem continuous_quotient_mk {α : Type u} {s : setoid α} :

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

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

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), 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 α} :
(𝓝 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)} (hi : i.finite) (hs : ∀ (a : ι), a iis_open (s a)) :
is_open (i.pi s)

theorem set_pi_mem_nhds {ι : Type u_1} {π : ι → Type u_2} [Π (a : ι), topological_space («π» a)] {i : set ι} {s : Π (a : ι), set («π» a)} {x : Π (a : ι), «π» a} (hi : i.finite) (hs : ∀ (a : ι), a is a 𝓝 (x a)) :
i.pi s 𝓝 x

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 ι] (hg : ∀ (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 σ)} :
∀ (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 σ)} :
∀ (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)] {f : → β} (h : ∀ (i : ι), continuous (λ (a : σ i), f i, a⟩)) :

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)} (hf : ∀ (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)] {f : → β} (h : ∀ (i : ι), is_open_map (λ (a : σ i), f i, a⟩)) :

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} (hf : ∀ (i : ι), embedding (f i)) :

The sum of embeddings is an embedding.

theorem continuous_ulift_down {α : Type u}  :

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

theorem mem_closure_of_continuous {α : Type u} {β : Type v} {f : α → β} {a : α} {s : set α} {t : set β} (hf : continuous f) (ha : a ) (h : s (closure t)) :
f a

theorem mem_closure_of_continuous2 {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {a : α} {b : β} {s : set α} {t : set β} {u : set γ} (hf : continuous (λ (p : α × β), f p.fst p.snd)) (ha : a ) (hb : b ) (h : ∀ (a : α), a s∀ (b : β), b tf a b ) :
f a b