# mathlib3documentation

topology.constructions

# Constructions of new topological spaces from old ones #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def subtype.topological_space {α : Type u} {p : α Prop} [t : topological_space α] :
Equations
@[protected, instance]
def quot.topological_space {α : Type u} {r : α α Prop} [t : topological_space α] :
Equations
@[protected, instance]
def quotient.topological_space {α : Type u} {s : setoid α} [t : topological_space α] :
Equations
@[protected, instance]
def prod.topological_space {α : Type u} {β : Type v} [t₁ : topological_space α] [t₂ : topological_space β] :
Equations
@[protected, instance]
def sum.topological_space {α : Type u} {β : Type v} [t₁ : topological_space α] [t₂ : topological_space β] :
Equations
@[protected, instance]
def sigma.topological_space {α : Type u} {β : α Type v} [t₂ : Π (a : α), topological_space (β a)] :
Equations
@[protected, instance]
def Pi.topological_space {α : Type u} {β : α Type v} [t₂ : Π (a : α), topological_space (β a)] :
topological_space (Π (a : α), β a)
Equations
@[protected, instance]
Equations

### `additive`, `multiplicative`#

The topology on those type synonyms is inherited without change.

@[protected, instance]
def additive.topological_space {α : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def additive.discrete_topology {α : Type u}  :
@[protected, instance]
theorem continuous_of_mul {α : Type u}  :
theorem continuous_to_mul {α : Type u}  :
theorem continuous_of_add {α : Type u}  :
theorem continuous_to_add {α : Type u}  :
theorem is_open_map_of_mul {α : Type u}  :
theorem is_open_map_to_mul {α : Type u}  :
theorem is_open_map_of_add {α : Type u}  :
theorem is_open_map_to_add {α : Type u}  :
theorem is_closed_map_of_mul {α : Type u}  :
theorem is_closed_map_to_mul {α : Type u}  :
theorem is_closed_map_of_add {α : Type u}  :
theorem is_closed_map_to_add {α : Type u}  :
theorem nhds_of_mul {α : Type u} (a : α) :
theorem nhds_of_add {α : Type u} (a : α) :
theorem nhds_to_mul {α : Type u} (a : additive α) :
theorem nhds_to_add {α : Type u} (a : multiplicative α) :

### Order dual #

The topology on this type synonym is inherited without change.

@[protected, instance]
Equations
@[protected, instance]
theorem continuous_to_dual {α : Type u}  :
theorem continuous_of_dual {α : Type u}  :
theorem is_open_map_to_dual {α : Type u}  :
theorem is_open_map_of_dual {α : Type u}  :
theorem is_closed_map_to_dual {α : Type u}  :
theorem is_closed_map_of_dual {α : Type u}  :
theorem nhds_to_dual {α : Type u} (a : α) :
theorem nhds_of_dual {α : Type u} (a : α) :
theorem quotient.preimage_mem_nhds {α : Type u} [s : setoid α] {V : set (quotient s)} {a : α} (hs : V ) :
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.

@[protected, instance]
def subtype.discrete_topology {α : Type u} {p : α Prop}  :
@[protected, instance]
def sum.discrete_topology {α : Type u} {β : Type v} [hα : discrete_topology α] [hβ : discrete_topology β] :
@[protected, 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 nhds a (u : set α) (H : u nhds a), t
theorem nhds_subtype {α : Type u} (s : set α) (a : {x // x s}) :
nhds a = (nhds a)
theorem nhds_within_subtype_eq_bot_iff {α : Type u} {s t : set α} {x : s} :
theorem nhds_ne_subtype_eq_bot_iff {α : Type u} {S : set α} {x : S} :
theorem nhds_ne_subtype_ne_bot_iff {α : Type u} {S : set α} {x : S} :
theorem discrete_topology_subtype_iff {α : Type u} {S : set α} :
(x : α), x S {x} =
def cofinite_topology (α : Type u_1) :
Type u_1

A type synonym equiped with the topology whose open sets are the empty set and the sets with finite complements.

Equations
Instances for `cofinite_topology`
def cofinite_topology.of {α : Type u} :

The identity equivalence between `α` and `cofinite_topology α`.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem cofinite_topology.mem_nhds_iff {α : Type u} {a : cofinite_topology α} {s : set } :
@[continuity]
theorem continuous_fst {α : Type u} {β : Type v}  :
theorem continuous.fst {α : Type u} {β : Type v} {γ : Type u_1} {f : α β × γ} (hf : continuous f) :
continuous (λ (a : α), (f a).fst)

Postcomposing `f` with `prod.fst` is continuous

theorem continuous.fst' {α : Type u} {β : Type v} {γ : Type u_1} {f : α γ} (hf : continuous f) :
continuous (λ (x : α × β), f x.fst)

Precomposing `f` with `prod.fst` is continuous

theorem continuous_at_fst {α : Type u} {β : Type v} {p : α × β} :
theorem continuous_at.fst {α : Type u} {β : Type v} {γ : Type u_1} {f : α β × γ} {x : α} (hf : x) :
continuous_at (λ (a : α), (f a).fst) x

Postcomposing `f` with `prod.fst` is continuous at `x`

theorem continuous_at.fst' {α : Type u} {β : Type v} {γ : Type u_1} {f : α γ} {x : α} {y : β} (hf : x) :
continuous_at (λ (x : α × β), f x.fst) (x, y)

Precomposing `f` with `prod.fst` is continuous at `(x, y)`

theorem continuous_at.fst'' {α : Type u} {β : Type v} {γ : Type u_1} {f : α γ} {x : α × β} (hf : x.fst) :
continuous_at (λ (x : α × β), f x.fst) x

Precomposing `f` with `prod.fst` is continuous at `x : α × β`

@[continuity]
theorem continuous_snd {α : Type u} {β : Type v}  :
theorem continuous.snd {α : Type u} {β : Type v} {γ : Type u_1} {f : α β × γ} (hf : continuous f) :
continuous (λ (a : α), (f a).snd)

Postcomposing `f` with `prod.snd` is continuous

theorem continuous.snd' {α : Type u} {β : Type v} {γ : Type u_1} {f : β γ} (hf : continuous f) :
continuous (λ (x : α × β), f x.snd)

Precomposing `f` with `prod.snd` is continuous

theorem continuous_at_snd {α : Type u} {β : Type v} {p : α × β} :
theorem continuous_at.snd {α : Type u} {β : Type v} {γ : Type u_1} {f : α β × γ} {x : α} (hf : x) :
continuous_at (λ (a : α), (f a).snd) x

Postcomposing `f` with `prod.snd` is continuous at `x`

theorem continuous_at.snd' {α : Type u} {β : Type v} {γ : Type u_1} {f : β γ} {x : α} {y : β} (hf : y) :
continuous_at (λ (x : α × β), f x.snd) (x, y)

Precomposing `f` with `prod.snd` is continuous at `(x, y)`

theorem continuous_at.snd'' {α : Type u} {β : Type v} {γ : Type u_1} {f : β γ} {x : α × β} (hf : x.snd) :
continuous_at (λ (x : α × β), f x.snd) x

Precomposing `f` with `prod.snd` is continuous at `x : α × β`

@[continuity]
theorem continuous.prod_mk {α : Type u} {β : Type v} {γ : Type u_1} {f : γ α} {g : γ β} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : γ), (f x, g x))
@[simp]
theorem continuous_prod_mk {α : Type u} {β : Type v} {γ : Type u_1} {f : α β} {g : α γ} :
continuous (λ (x : α), (f x, g x))
@[continuity]
theorem continuous.prod.mk {α : Type u} {β : Type v} (a : α) :
continuous (λ (b : β), (a, b))
@[continuity]
theorem continuous.prod.mk_left {α : Type u} {β : Type v} (b : β) :
continuous (λ (a : α), (a, b))
theorem continuous.comp₂ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {g : α × β γ} (hg : continuous g) {e : δ α} (he : continuous e) {f : δ β} (hf : continuous f) :
continuous (λ (x : δ), g (e x, f x))
theorem continuous.comp₃ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {ε : Type u_3} {g : α × β × γ ε} (hg : continuous g) {e : δ α} (he : continuous e) {f : δ β} (hf : continuous f) {k : δ γ} (hk : continuous k) :
continuous (λ (x : δ), g (e x, f x, k x))
theorem continuous.comp₄ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {ε : Type u_3} {ζ : Type u_4} {g : α × β × γ × ζ ε} (hg : continuous g) {e : δ α} (he : continuous e) {f : δ β} (hf : continuous f) {k : δ γ} (hk : continuous k) {l : δ ζ} (hl : continuous l) :
continuous (λ (x : δ), g (e x, f x, k x, l x))
theorem continuous.prod_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : γ α} {g : δ β} (hf : continuous f) (hg : continuous g) :
continuous (λ (x : γ × δ), (f x.fst, g x.snd))
theorem continuous_inf_dom_left₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β γ} {ta1 ta2 : topological_space α} {tb1 tb2 : topological_space β} {tc1 : topological_space γ} (h : continuous (λ (p : α × β), f p.fst p.snd)) :
continuous (λ (p : α × β), f p.fst p.snd)

A version of `continuous_inf_dom_left` for binary functions

theorem continuous_inf_dom_right₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β γ} {ta1 ta2 : topological_space α} {tb1 tb2 : topological_space β} {tc1 : topological_space γ} (h : continuous (λ (p : α × β), f p.fst p.snd)) :
continuous (λ (p : α × β), f p.fst p.snd)

A version of `continuous_inf_dom_right` for binary functions

theorem continuous_Inf_dom₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α β γ} {tas : set } {tbs : set } {ta : topological_space α} {tb : topological_space β} {tc : topological_space γ} (ha : ta tas) (hb : tb tbs) (hf : continuous (λ (p : α × β), f p.fst p.snd)) :
continuous (λ (p : α × β), f p.fst p.snd)

A version of `continuous_Inf_dom` for binary functions

theorem filter.eventually.prod_inl_nhds {α : Type u} {β : Type v} {p : α Prop} {a : α} (h : ∀ᶠ (x : α) in nhds a, p x) (b : β) :
∀ᶠ (x : α × β) in nhds (a, b), p x.fst
theorem filter.eventually.prod_inr_nhds {α : Type u} {β : Type v} {p : β Prop} {b : β} (h : ∀ᶠ (x : β) in nhds b, p x) (a : α) :
∀ᶠ (x : α × β) in nhds (a, b), p x.snd
theorem filter.eventually.prod_mk_nhds {α : Type u} {β : Type v} {pa : α Prop} {a : α} (ha : ∀ᶠ (x : α) in nhds a, pa x) {pb : β Prop} {b : β} (hb : ∀ᶠ (y : β) in nhds b, pb y) :
∀ᶠ (p : α × β) in nhds (a, b), pa p.fst pb p.snd
theorem continuous_swap {α : Type u} {β : Type v}  :
theorem continuous_uncurry_left {α : Type u} {β : Type v} {γ : Type u_1} {f : α β γ} (a : α) (h : continuous ) :
theorem continuous_uncurry_right {α : Type u} {β : Type v} {γ : Type u_1} {f : α β γ} (b : β) (h : continuous ) :
continuous (λ (a : α), f a b)
theorem continuous_curry {α : Type u} {β : Type v} {γ : Type u_1} {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 : β} :
nhds (a, b) = (nhds a).prod (nhds b)
theorem continuous_uncurry_of_discrete_topology {α : Type u} {β : Type v} {γ : Type u_1} {f : α β γ} (hf : (a : α), continuous (f a)) :

If a function `f x y` is such that `y ↦ f x y` is continuous for all `x`, and `x` lives in a discrete space, then `f` is continuous.

theorem mem_nhds_prod_iff {α : Type u} {β : Type v} {a : α} {b : β} {s : set × β)} :
s nhds (a, b) (u : set α) (H : u nhds a) (v : set β) (H : v nhds b), u ×ˢ v s
theorem mem_nhds_prod_iff' {α : Type u} {β : Type v} {a : α} {b : β} {s : set × β)} :
s nhds (a, b) (u : set α) (v : set β), a u b v u ×ˢ v s
theorem prod.tendsto_iff {β : Type v} {γ : Type u_1} {α : Type u_2} (seq : α β × γ) {f : filter α} (x : β × γ) :
f (nhds x) filter.tendsto (λ (n : α), (seq n).fst) f (nhds x.fst) filter.tendsto (λ (n : α), (seq n).snd) f (nhds x.snd)
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 : (nhds a).has_basis pa sa) (hb : (nhds b).has_basis pb sb) :
(nhds (a, b)).has_basis (λ (i : ιa × ιb), pa i.fst pb i.snd) (λ (i : ιa × ιb), sa i.fst ×ˢ sb i.snd)
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 β} {ab : α × β} (ha : (nhds ab.fst).has_basis pa sa) (hb : (nhds ab.snd).has_basis pb sb) :
(nhds ab).has_basis (λ (i : ιa × ιb), pa i.fst pb i.snd) (λ (i : ιa × ιb), sa i.fst ×ˢ sb i.snd)
@[protected, instance]
def prod.discrete_topology {α : Type u} {β : Type v}  :
theorem prod_mem_nhds_iff {α : Type u} {β : Type v} {s : set α} {t : set β} {a : α} {b : β} :
s ×ˢ t nhds (a, b) s nhds a t nhds b
theorem prod_mem_nhds {α : Type u} {β : Type v} {s : set α} {t : set β} {a : α} {b : β} (ha : s nhds a) (hb : t nhds b) :
s ×ˢ t nhds (a, b)
theorem filter.eventually.prod_nhds {α : Type u} {β : Type v} {p : α Prop} {q : β Prop} {a : α} {b : β} (ha : ∀ᶠ (x : α) in nhds a, p x) (hb : ∀ᶠ (y : β) in nhds b, q y) :
∀ᶠ (z : α × β) in nhds (a, b), p z.fst q z.snd
theorem nhds_swap {α : Type u} {β : Type v} (a : α) (b : β) :
nhds (a, b) = (nhds (b, a))
theorem filter.tendsto.prod_mk_nhds {α : Type u} {β : Type v} {γ : Type u_1} {a : α} {b : β} {f : filter γ} {ma : γ α} {mb : γ β} (ha : f (nhds a)) (hb : f (nhds b)) :
filter.tendsto (λ (c : γ), (ma c, mb c)) f (nhds (a, b))
theorem filter.eventually.curry_nhds {α : Type u} {β : Type v} {p : α × β Prop} {x : α} {y : β} (h : ∀ᶠ (x : α × β) in nhds (x, y), p x) :
∀ᶠ (x' : α) in nhds x, ∀ᶠ (y' : β) in nhds y, p (x', y')
theorem continuous_at.prod {α : Type u} {β : Type v} {γ : Type u_1} {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 u_1} {δ : Type u_2} {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 u_1} {δ : Type u_2} {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 ×ˢ v}
theorem prod_eq_generate_from {α : Type u} {β : Type v}  :
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 ×ˢ v s)
theorem prod_induced_induced {β : Type v} {δ : Type u_2} {α : Type u_1} {γ : Type u_3} (f : α β) (g : γ δ) :

A product of induced topologies is induced by the product map

theorem continuous_uncurry_of_discrete_topology_left {α : Type u} {β : Type v} {γ : Type u_1} {f : α β γ} (h : (a : α), continuous (f a)) :
theorem exists_nhds_square {α : Type u} {s : set × α)} {x : α} (hx : s nhds (x, x)) :
(U : set α), x U U ×ˢ U s

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

theorem map_fst_nhds_within {α : Type u} {β : Type v} (x : α × β) :

`prod.fst` maps neighborhood of `x : α × β` within the section `prod.snd ⁻¹' {x.2}` to `𝓝 x.1`.

@[simp]
theorem map_fst_nhds {α : Type u} {β : Type v} (x : α × β) :
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 map_snd_nhds_within {α : Type u} {β : Type v} (x : α × β) :

`prod.snd` maps neighborhood of `x : α × β` within the section `prod.fst ⁻¹' {x.1}` to `𝓝 x.2`.

@[simp]
theorem map_snd_nhds {α : Type u} {β : Type v} (x : α × β) :
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 interior_prod_eq {α : Type u} {β : Type v} (s : set α) (t : set β) :
interior (s ×ˢ t) =
theorem frontier_prod_eq {α : Type u} {β : Type v} (s : set α) (t : set β) :
@[simp]
theorem frontier_prod_univ_eq {α : Type u} {β : Type v} (s : set α) :
@[simp]
theorem frontier_univ_prod_eq {α : Type u} {β : Type v} (s : set β) :
theorem map_mem_closure₂ {α : Type u} {β : Type v} {γ : Type u_1} {f : α β γ} {a : α} {b : β} {s : set α} {t : set β} {u : set γ} (hf : continuous ) (ha : a ) (hb : b ) (h : (a : α), a s (b : β), b t f 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₁ ×ˢ s₂)
theorem dense.prod {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : dense s) (ht : dense t) :
dense (s ×ˢ t)

The product of two dense sets is a dense set.

theorem dense_range.prod_map {β : Type v} {γ : Type u_1} {ι : Type u_2} {κ : Type u_3} {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 u_1} {δ : Type u_2} {f : α β} {g : γ δ} (hf : inducing f) (hg : inducing g) :
inducing (λ (x : α × γ), (f x.fst, g x.snd))
@[simp]
theorem inducing_const_prod {α : Type u} {β : Type v} {γ : Type u_1} {a : α} {f : β γ} :
inducing (λ (x : β), (a, f x))
@[simp]
theorem inducing_prod_const {α : Type u} {β : Type v} {γ : Type u_1} {b : β} {f : α γ} :
inducing (λ (x : α), (f x, b))
theorem embedding.prod_mk {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α β} {g : γ δ} (hf : embedding f) (hg : embedding g) :
embedding (λ (x : α × γ), (f x.fst, g x.snd))
@[protected]
theorem is_open_map.prod {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α β} {g : γ δ} (hf : is_open_map f) (hg : is_open_map g) :
is_open_map (λ (p : α × γ), (f p.fst, g p.snd))
@[protected]
theorem open_embedding.prod {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {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))
@[continuity]
theorem continuous_inl {α : Type u} {β : Type v}  :
@[continuity]
theorem continuous_inr {α : Type u} {β : Type v}  :
theorem is_open_sum_iff {α : Type u} {β : Type v} {s : set β)} :
theorem is_open_map_inl {α : Type u} {β : Type v}  :
theorem is_open_map_inr {α : Type u} {β : Type v}  :
theorem open_embedding_inl {α : Type u} {β : Type v}  :
theorem open_embedding_inr {α : Type u} {β : Type v}  :
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 is_closed_range_inl {α : Type u} {β : Type v}  :
theorem is_closed_range_inr {α : Type u} {β : Type v}  :
theorem closed_embedding_inl {α : Type u} {β : Type v}  :
theorem closed_embedding_inr {α : Type u} {β : Type v}  :
theorem nhds_inl {α : Type u} {β : Type v} (x : α) :
theorem nhds_inr {α : Type u} {β : Type v} (x : β) :
theorem continuous_sum_dom {α : Type u} {β : Type v} {γ : Type u_1} {f : α β γ} :
theorem continuous_sum_elim {α : Type u} {β : Type v} {γ : Type u_1} {f : α γ} {g : β γ} :
@[continuity]
theorem continuous.sum_elim {α : Type u} {β : Type v} {γ : Type u_1} {f : α γ} {g : β γ} (hf : continuous f) (hg : continuous g) :
@[simp]
theorem continuous_sum_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α β} {g : γ δ} :
@[continuity]
theorem continuous.sum_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} {f : α β} {g : γ δ} (hf : continuous f) (hg : continuous g) :
theorem is_open_map_sum {α : Type u} {β : Type v} {γ : Type u_1} {f : α β γ} :
is_open_map (λ (a : α), f (sum.inl a)) is_open_map (λ (b : β), f (sum.inr b))
@[simp]
theorem is_open_map_sum_elim {α : Type u} {β : Type v} {γ : Type u_1} {f : α γ} {g : β γ} :
theorem is_open_map.sum_elim {α : Type u} {β : Type v} {γ : Type u_1} {f : α γ} {g : β γ} (hf : is_open_map f) (hg : is_open_map g) :
theorem inducing_coe {β : Type v} {b : set β} :
theorem inducing.of_cod_restrict {α : Type u} {β : Type v} {f : α β} {b : set β} (hb : (a : α), f a b) (h : inducing b hb)) :
theorem embedding_subtype_coe {α : Type u} {p : α Prop} :
theorem closed_embedding_subtype_coe {α : Type u} {p : α Prop} (h : is_closed {a : α | p a}) :
@[continuity]
theorem continuous_subtype_val {α : Type u} {p : α Prop} :
theorem continuous_subtype_coe {α : Type u} {p : α Prop} :
theorem continuous.subtype_coe {α : Type u} {β : Type v} {p : α Prop} {f : β } (hf : continuous f) :
continuous (λ (x : β), (f x))
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) :
@[continuity]
theorem continuous.subtype_mk {α : Type u} {β : Type v} {p : α Prop} {f : β α} (h : continuous f) (hp : (x : β), p (f x)) :
continuous (λ (x : β), f x, _⟩)
theorem continuous.subtype_map {α : Type u} {β : Type v} {p : α Prop} {f : α β} (h : continuous f) {q : β Prop} (hpq : (x : α), p x q (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 subtype.dense_iff {α : Type u} {s : set α} {t : set s} :
theorem map_nhds_subtype_coe_eq {α : Type u} {p : α Prop} {a : α} (ha : p a) (h : {a : α | p a} nhds a) :
(nhds a, ha⟩) = nhds a
theorem nhds_subtype_eq_comap {α : Type u} {p : α Prop} {a : α} {h : p a} :
nhds a, h⟩ = (nhds a)
theorem tendsto_subtype_rng {α : Type u} {β : Type u_1} {p : α Prop} {b : filter β} {f : β } {a : subtype p} :
(nhds a) filter.tendsto (λ (x : β), (f x)) b (nhds a)
theorem closure_subtype {α : Type u} {p : α Prop} {x : {a // p a}} {s : set {a // p a}} :
theorem continuous_at_cod_restrict_iff {α : Type u} {β : Type v} {f : α β} {t : set β} (h1 : (x : α), f x t) {x : α} :
theorem continuous_at.cod_restrict {α : Type u} {β : Type v} {f : α β} {t : set β} (h1 : (x : α), f x t) {x : α} :

Alias of the reverse direction of `continuous_at_cod_restrict_iff`.

theorem continuous_at.restrict {α : Type u} {β : Type v} {f : α β} {s : set α} {t : set β} (h1 : s t) {x : s} (h2 : x) :
theorem continuous_at.restrict_preimage {α : Type u} {β : Type v} {f : α β} {s : set β} {x : (f ⁻¹' s)} (h : x) :
x
@[continuity]
theorem continuous.cod_restrict {α : Type u} {β : Type v} {f : α β} {s : set β} (hf : continuous f) (hs : (a : α), f a s) :
theorem inducing.cod_restrict {α : Type u} {β : Type v} {e : α β} (he : inducing e) {s : set β} (hs : (x : α), e x s) :
inducing s hs)
theorem embedding.cod_restrict {α : Type u} {β : Type v} {e : α β} (he : embedding e) (s : set β) (hs : (x : α), e x s) :
embedding s hs)
theorem embedding_inclusion {α : Type u} {s t : set α} (h : s t) :
theorem discrete_topology.of_subset {X : Type u_1} {s t : set X} (ds : discrete_topology s) (ts : t s) :

Let `s, t ⊆ X` be two subsets of a topological space `X`. If `t ⊆ s` and the topology induced by `X`on `s` is discrete, then also the topology induces on `t` is discrete.

theorem quotient_map_quot_mk {α : Type u} {r : α α Prop} :
quotient_map (quot.mk r)
@[continuity]
theorem continuous_quot_mk {α : Type u} {r : α α Prop} :
continuous (quot.mk r)
@[continuity]
theorem continuous_quot_lift {α : Type u} {β : Type v} {r : α α Prop} {f : α β} (hr : (a b : α), r a b f 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 : α β} (h : continuous f) (hs : (a b : α), a b f a = f b) :
theorem continuous.quotient_lift_on' {α : Type u} {β : Type v} {s : setoid α} {f : α β} (h : continuous f) (hs : (a b : α), b f a = f b) :
continuous (λ (x : quotient s), x.lift_on' f hs)
theorem continuous.quotient_map' {α : Type u} {β : Type v} {s : setoid α} {t : setoid β} {f : α β} (hf : continuous f) (H : f f) :
theorem continuous_pi_iff {α : Type u} {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} :
(i : ι), continuous (λ (a : α), f a i)
@[continuity]
theorem continuous_pi {α : Type u} {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} (h : (i : ι), continuous (λ (a : α), f a i)) :
@[continuity]
theorem continuous_apply {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] (i : ι) :
continuous (λ (p : Π (i : ι), π i), p i)
@[continuity]
theorem continuous_apply_apply {ι : Type u_5} {κ : Type u_7} {ρ : κ ι Type u_1} [Π (j : κ) (i : ι), topological_space (ρ j i)] (j : κ) (i : ι) :
continuous (λ (p : Π (j : κ) (i : ι), ρ j i), p j i)
theorem continuous_at_apply {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] (i : ι) (x : Π (i : ι), π i) :
continuous_at (λ (p : Π (i : ι), π i), p i) x
theorem filter.tendsto.apply {β : Type v} {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {l : filter β} {f : β Π (i : ι), π i} {x : Π (i : ι), π i} (h : (nhds x)) (i : ι) :
filter.tendsto (λ (a : β), f a i) l (nhds (x i))
theorem nhds_pi {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {a : Π (i : ι), π i} :
nhds a = filter.pi (λ (i : ι), nhds (a i))
theorem tendsto_pi_nhds {β : Type v} {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f : β Π (i : ι), π i} {g : Π (i : ι), π i} {u : filter β} :
(nhds g) (x : ι), filter.tendsto (λ (i : β), f i x) u (nhds (g x))
theorem continuous_at_pi {α : Type u} {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} {x : α} :
(i : ι), continuous_at (λ (y : α), f y i) x
theorem filter.tendsto.update {β : Type v} {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] [decidable_eq ι] {l : filter β} {f : β Π (i : ι), π i} {x : Π (i : ι), π i} (hf : (nhds x)) (i : ι) {g : β π i} {xi : π i} (hg : (nhds xi)) :
filter.tendsto (λ (a : β), function.update (f a) i (g a)) l (nhds i xi))
theorem continuous_at.update {α : Type u} {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} [decidable_eq ι] {a : α} (hf : a) (i : ι) {g : α π i} (hg : a) :
continuous_at (λ (a : α), function.update (f a) i (g a)) a
theorem continuous.update {α : Type u} {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} [decidable_eq ι] (hf : continuous f) (i : ι) {g : α π i} (hg : continuous g) :
continuous (λ (a : α), function.update (f a) i (g a))
@[continuity]
theorem continuous_update {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] [decidable_eq ι] (i : ι) :
continuous (λ (f : (Π (j : ι), π j) × π i), f.snd)

`function.update f i x` is continuous in `(f, x)`.

@[continuity]
theorem continuous_single {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] [Π (i : ι), has_zero (π i)] [decidable_eq ι] (i : ι) :
continuous (λ (x : π i), x)

`pi.single i x` is continuous in `x`.

@[continuity]
theorem continuous_mul_single {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] [Π (i : ι), has_one (π i)] [decidable_eq ι] (i : ι) :
continuous (λ (x : π i), x)

`pi.mul_single i x` is continuous in `x`.

theorem filter.tendsto.fin_insert_nth {β : Type v} {n : } {π : fin (n + 1) Type u_1} [Π (i : fin (n + 1)), topological_space (π i)] (i : fin (n + 1)) {f : β π i} {l : filter β} {x : π i} (hf : (nhds x)) {g : β Π (j : fin n), π ((i.succ_above) j)} {y : Π (j : fin n), π ((i.succ_above) j)} (hg : (nhds y)) :
filter.tendsto (λ (a : β), i.insert_nth (f a) (g a)) l (nhds (i.insert_nth x y))
theorem continuous_at.fin_insert_nth {α : Type u} {n : } {π : fin (n + 1) Type u_1} [Π (i : fin (n + 1)), topological_space (π i)] (i : fin (n + 1)) {f : α π i} {a : α} (hf : a) {g : α Π (j : fin n), π ((i.succ_above) j)} (hg : a) :
continuous_at (λ (a : α), i.insert_nth (f a) (g a)) a
theorem continuous.fin_insert_nth {α : Type u} {n : } {π : fin (n + 1) Type u_1} [Π (i : fin (n + 1)), topological_space (π i)] (i : fin (n + 1)) {f : α π i} (hf : continuous f) {g : α Π (j : fin n), π ((i.succ_above) j)} (hg : continuous g) :
continuous (λ (a : α), i.insert_nth (f a) (g a))
theorem is_open_set_pi {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {i : set ι} {s : Π (a : ι), set (π a)} (hi : i.finite) (hs : (a : ι), a i is_open (s a)) :
is_open (i.pi s)
theorem is_open_pi_iff {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {s : set (Π (a : ι), π a)} :
(f : Π (a : ι), π a), f s ( (I : finset ι) (u : Π (a : ι), set (π a)), ( (a : ι), a I is_open (u a) f a u a) I.pi u s)
theorem is_open_pi_iff' {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] [finite ι] {s : set (Π (a : ι), π a)} :
(f : Π (a : ι), π a), f s ( (u : Π (a : ι), set (π a)), ( (a : ι), is_open (u a) f a u a) s)
theorem is_closed_set_pi {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {i : set ι} {s : Π (a : ι), set (π a)} (hs : (a : ι), a i is_closed (s a)) :
theorem mem_nhds_of_pi_mem_nhds {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {I : set ι} {s : Π (i : ι), set (π i)} (a : Π (i : ι), π i) (hs : I.pi s nhds a) {i : ι} (hi : i I) :
s i nhds (a i)
theorem set_pi_mem_nhds {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {i : set ι} {s : Π (a : ι), set (π a)} {x : Π (a : ι), π a} (hi : i.finite) (hs : (a : ι), a i s a nhds (x a)) :
i.pi s nhds x
theorem set_pi_mem_nhds_iff {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {I : set ι} (hI : I.finite) {s : Π (i : ι), set (π i)} (a : Π (i : ι), π i) :
I.pi s nhds a (i : ι), i I s i nhds (a i)
theorem interior_pi_set {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {I : set ι} (hI : I.finite) {s : Π (i : ι), set (π i)} :
interior (I.pi s) = I.pi (λ (i : ι), interior (s i))
theorem exists_finset_piecewise_mem_of_mem_nhds {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] [decidable_eq ι] {s : set (Π (a : ι), π a)} {x : Π (a : ι), π a} (hs : s nhds x) (y : Π (a : ι), π a) :
(I : finset ι), I.piecewise x y s
theorem pi_eq_generate_from {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] :
Pi.topological_space = topological_space.generate_from {g : set (Π (a : ι), π a) | (s : Π (a : ι), set (π a)) (i : finset ι), ( (a : ι), a i is_open (s a)) g = i.pi s}
theorem pi_generate_from_eq {ι : Type u_5} {π : ι Type u_1} {g : Π (a : ι), set (set (π a))} :
Pi.topological_space = topological_space.generate_from {t : set (Π (a : ι), π a) | (s : Π (a : ι), set (π a)) (i : finset ι), ( (a : ι), a i s a g a) t = i.pi s}
theorem pi_generate_from_eq_finite {ι : Type u_5} {π : ι Type u_1} {g : Π (a : ι), set (set (π a))} [finite ι] (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 inducing_infi_to_pi {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] {X : Type u_1} (f : Π (i : ι), X π i) :
inducing (λ (x : X) (i : ι), f i x)

Suppose `π i` is a family of topological spaces indexed by `i : ι`, and `X` is a type endowed with a family of maps `f i : X → π i` for every `i : ι`, hence inducing a map `g : X → Π i, π i`. This lemma shows that infimum of the topologies on `X` induced by the `f i` as `i : ι` varies is simply the topology on `X` induced by `g : X → Π i, π i` where `Π i, π i` is endowed with the usual product topology.

@[protected, instance]
def Pi.discrete_topology {ι : Type u_5} {π : ι Type u_6} [Π (i : ι), topological_space (π i)] [finite ι] [ (i : ι), discrete_topology (π i)] :
discrete_topology (Π (i : ι), π i)

A finite product of discrete spaces is discrete.

@[continuity]
theorem continuous_sigma_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {i : ι} :
theorem is_open_sigma_iff {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {s : set (sigma σ)} :
(i : ι), is_open (sigma.mk i ⁻¹' s)
theorem is_closed_sigma_iff {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {s : set (sigma σ)} :
(i : ι), is_closed (sigma.mk i ⁻¹' s)
theorem is_open_map_sigma_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {i : ι} :
theorem is_open_range_sigma_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {i : ι} :
theorem is_closed_map_sigma_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {i : ι} :
theorem is_closed_range_sigma_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {i : ι} :
theorem open_embedding_sigma_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {i : ι} :
theorem closed_embedding_sigma_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {i : ι} :
theorem embedding_sigma_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {i : ι} :
theorem sigma.nhds_mk {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] (i : ι) (x : σ i) :
nhds i, x⟩ = (nhds x)
theorem sigma.nhds_eq {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] (x : sigma σ) :
nhds x = (nhds x.snd)
theorem comap_sigma_mk_nhds {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] (i : ι) (x : σ i) :
(nhds i, x⟩) = nhds x
theorem is_open_sigma_fst_preimage {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] (s : set ι) :
@[simp]
theorem continuous_sigma_iff {α : Type u} {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {f : α} :
(i : ι), continuous (λ (a : σ i), f i, a⟩)

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

@[continuity]
theorem continuous_sigma {α : Type u} {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {f : α} (hf : (i : ι), continuous (λ (a : σ i), f i, a⟩)) :

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

@[simp]
theorem continuous_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ι Type u_7} {τ : κ Type u_8} [Π (i : ι), topological_space (σ i)] [Π (k : κ), topological_space (τ k)] {f₁ : ι κ} {f₂ : Π (i : ι), σ i τ (f₁ i)} :
continuous (sigma.map f₁ f₂) (i : ι), continuous (f₂ i)
@[continuity]
theorem continuous.sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ι Type u_7} {τ : κ Type u_8} [Π (i : ι), topological_space (σ i)] [Π (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 u} {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] {f : α} :
(i : ι), is_open_map (λ (a : σ i), f i, a⟩)
theorem is_open_map_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ι Type u_7} {τ : κ Type u_8} [Π (i : ι), topological_space (σ i)] [Π (k : κ), topological_space (τ k)] {f₁ : ι κ} {f₂ : Π (i : ι), σ i τ (f₁ i)} :
is_open_map (sigma.map f₁ f₂) (i : ι), is_open_map (f₂ i)
theorem inducing_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ι Type u_7} {τ : κ Type u_8} [Π (i : ι), topological_space (σ i)] [Π (k : κ), topological_space (τ k)] {f₁ : ι κ} {f₂ : Π (i : ι), σ i τ (f₁ i)} (h₁ : function.injective f₁) :
inducing (sigma.map f₁ f₂) (i : ι), inducing (f₂ i)
theorem embedding_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ι Type u_7} {τ : κ Type u_8} [Π (i : ι), topological_space (σ i)] [Π (k : κ), topological_space (τ k)] {f₁ : ι κ} {f₂ : Π (i : ι), σ i τ (f₁ i)} (h : function.injective f₁) :
embedding (sigma.map f₁ f₂) (i : ι), embedding (f₂ i)
theorem open_embedding_sigma_map {ι : Type u_5} {κ : Type u_6} {σ : ι Type u_7} {τ : κ Type u_8} [Π (i : ι), topological_space (σ i)] [Π (k : κ), topological_space (τ k)] {f₁ : ι κ} {f₂ : Π (i : ι), σ i τ (f₁ i)} (h : function.injective f₁) :
open_embedding (sigma.map f₁ f₂) (i : ι), open_embedding (f₂ i)
@[continuity]
theorem continuous_ulift_down {α : Type u}  :
@[continuity]
theorem continuous_ulift_up {α : Type u}  :
continuous ulift.up
theorem embedding_ulift_down {α : Type u}  :
theorem ulift.closed_embedding_down {α : Type u}  :
@[protected, instance]
def ulift.discrete_topology {α : Type u}  :