mathlib3 documentation

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 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

additive, multiplicative #

The topology on those type synonyms is inherited without change.

@[protected, instance]
Equations

Order dual #

The topology on this type synonym is inherited without change.

@[protected, instance]
Equations
theorem quotient.preimage_mem_nhds {α : Type u} [topological_space α] [s : setoid α] {V : set (quotient s)} {a : α} (hs : V nhds a) :
theorem dense.quotient {α : Type u} [setoid α] [topological_space α] {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 α] [topological_space α] {f : β α} (hf : dense_range f) :

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

@[protected, instance]
@[protected, instance]
@[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} [topological_space α] (s : set α) (a : {x // x s}) (t : set {x // x s}) :
t nhds a (u : set α) (H : u nhds a), coe ⁻¹' u t
theorem nhds_subtype {α : Type u} [topological_space α] (s : set α) (a : {x // x s}) :
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

The identity equivalence between α and cofinite_topology α.

Equations
@[continuity]
theorem continuous.fst {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {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} [topological_space α] [topological_space β] [topological_space γ] {f : α γ} (hf : continuous f) :
continuous (λ (x : α × β), f x.fst)

Precomposing f with prod.fst is continuous

theorem continuous_at_fst {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α × β} :
theorem continuous_at.fst {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α β × γ} {x : α} (hf : continuous_at f 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} [topological_space α] [topological_space β] [topological_space γ] {f : α γ} {x : α} {y : β} (hf : continuous_at f 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} [topological_space α] [topological_space β] [topological_space γ] {f : α γ} {x : α × β} (hf : continuous_at f 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} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {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} [topological_space α] [topological_space β] [topological_space γ] {f : β γ} (hf : continuous f) :
continuous (λ (x : α × β), f x.snd)

Precomposing f with prod.snd is continuous

theorem continuous_at_snd {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α × β} :
theorem continuous_at.snd {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α β × γ} {x : α} (hf : continuous_at f 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} [topological_space α] [topological_space β] [topological_space γ] {f : β γ} {x : α} {y : β} (hf : continuous_at f 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} [topological_space α] [topological_space β] [topological_space γ] {f : β γ} {x : α × β} (hf : continuous_at f 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} [topological_space α] [topological_space β] [topological_space γ] {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} [topological_space α] [topological_space β] [topological_space γ] {f : α β} {g : α γ} :
continuous (λ (x : α), (f x, g x)) continuous f continuous g
@[continuity]
theorem continuous.prod.mk {α : Type u} {β : Type v} [topological_space α] [topological_space β] (a : α) :
continuous (λ (b : β), (a, b))
@[continuity]
theorem continuous.prod.mk_left {α : Type u} {β : Type v} [topological_space α] [topological_space β] (b : β) :
continuous (λ (a : α), (a, b))
theorem continuous.comp₂ {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] [topological_space ε] {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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] [topological_space ε] [topological_space ζ] {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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {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 (topological_space α)} {tbs : set (topological_space β)} {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} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] {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_uncurry_left {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α β γ} (a : α) (h : continuous (function.uncurry f)) :
theorem continuous_uncurry_right {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α β γ} (b : β) (h : continuous (function.uncurry f)) :
continuous (λ (a : α), f a b)
theorem continuous_curry {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {g : α × β γ} (a : α) (h : continuous g) :
theorem is_open.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : set α} {t : set β} (hs : is_open s) (ht : is_open t) :
theorem nhds_prod_eq {α : Type u} {β : Type v} [topological_space α] [topological_space β] {a : α} {b : β} :
nhds (a, b) = (nhds a).prod (nhds b)
theorem continuous_uncurry_of_discrete_topology {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] [discrete_topology α] {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} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] {a : α} {b : β} {s : set × β)} :
s nhds (a, b) (u : set α) (v : set β), is_open u a u is_open v b v u ×ˢ v s
theorem prod.tendsto_iff {β : Type v} {γ : Type u_1} [topological_space β] [topological_space γ] {α : Type u_2} (seq : α β × γ) {f : filter α} (x : β × γ) :
filter.tendsto seq 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} [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 : β} (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} [topological_space α] [topological_space β] {ι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]
theorem prod_mem_nhds_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] (a : α) (b : β) :
nhds (a, b) = filter.map prod.swap (nhds (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 : γ β} (ha : filter.tendsto ma f (nhds a)) (hb : filter.tendsto mb f (nhds b)) :
filter.tendsto (λ (c : γ), (ma c, mb c)) f (nhds (a, b))
theorem filter.eventually.curry_nhds {α : Type u} {β : Type v} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] [topological_space γ] {f : α β} {g : α γ} {x : α} (hf : continuous_at f x) (hg : continuous_at g x) :
continuous_at (λ (x : α), (f x, g x)) x
theorem continuous_at.prod_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α γ} {g : β δ} {p : α × β} (hf : continuous_at f p.fst) (hg : continuous_at g 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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α γ} {g : β δ} {x : α} {y : β} (hf : continuous_at f x) (hg : continuous_at g 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 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 ×ˢ v s)
theorem prod_induced_induced {β : Type v} {δ : Type u_2} [topological_space β] [topological_space δ] {α : 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} [topological_space α] [topological_space β] [topological_space γ] [discrete_topology α] {f : α β γ} (h : (a : α), continuous (f a)) :
theorem exists_nhds_square {α : Type u} [topological_space α] {s : set × α)} {x : α} (hx : s nhds (x, x)) :
(U : set α), is_open U 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} [topological_space α] [topological_space β] (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} [topological_space α] [topological_space β] (x : α × β) :

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

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

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 interior_prod_eq {α : Type u} {β : Type v} [topological_space α] [topological_space β] (s : set α) (t : set β) :
theorem frontier_prod_eq {α : Type u} {β : Type v} [topological_space α] [topological_space β] (s : set α) (t : set β) :
@[simp]
@[simp]
theorem map_mem_closure₂ {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α β γ} {a : α} {b : β} {s : set α} {t : set β} {u : set γ} (hf : continuous (function.uncurry f)) (ha : a closure s) (hb : b closure t) (h : (a : α), a s (b : β), b t f a b u) :
f a b closure u
theorem is_closed.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s₁ : set α} {s₂ : set β} (h₁ : is_closed s₁) (h₂ : is_closed s₂) :
is_closed (s₁ ×ˢ s₂)
theorem dense.prod {α : Type u} {β : Type v} [topological_space α] [topological_space β] {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} [topological_space β] [topological_space γ] {ι : 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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {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} [topological_space α] [topological_space β] [topological_space γ] {a : α} {f : β γ} :
inducing (λ (x : β), (a, f x)) inducing f
@[simp]
theorem inducing_prod_const {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {b : β} {f : α γ} :
inducing (λ (x : α), (f x, b)) inducing f
theorem embedding.prod_mk {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {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} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {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} [topological_space α] [topological_space β] {f : α β} (hf : continuous f) :
embedding (λ (x : α), (x, f x))
@[continuity]
@[continuity]
theorem nhds_inl {α : Type u} {β : Type v} [topological_space α] [topological_space β] (x : α) :
theorem nhds_inr {α : Type u} {β : Type v} [topological_space α] [topological_space β] (x : β) :
theorem continuous_sum_dom {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α β γ} :
theorem continuous_sum_elim {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α γ} {g : β γ} :
@[continuity]
theorem continuous.sum_elim {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α γ} {g : β γ} (hf : continuous f) (hg : continuous g) :
@[simp]
theorem continuous_sum_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α β} {g : γ δ} :
@[continuity]
theorem continuous.sum_map {α : Type u} {β : Type v} {γ : Type u_1} {δ : Type u_2} [topological_space α] [topological_space β] [topological_space γ] [topological_space δ] {f : α β} {g : γ δ} (hf : continuous f) (hg : continuous g) :
theorem is_open_map_sum {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α β γ} :
is_open_map 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} [topological_space α] [topological_space β] [topological_space γ] {f : α γ} {g : β γ} :
theorem is_open_map.sum_elim {α : Type u} {β : Type v} {γ : Type u_1} [topological_space α] [topological_space β] [topological_space γ] {f : α γ} {g : β γ} (hf : is_open_map f) (hg : is_open_map g) :
theorem inducing_coe {β : Type v} [topological_space β] {b : set β} :
theorem inducing.of_cod_restrict {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α β} {b : set β} (hb : (a : α), f a b) (h : inducing (set.cod_restrict f b hb)) :
theorem embedding_subtype_coe {α : Type u} [topological_space α] {p : α Prop} :
theorem closed_embedding_subtype_coe {α : Type u} [topological_space α] {p : α Prop} (h : is_closed {a : α | p a}) :
@[continuity]
theorem continuous_subtype_val {α : Type u} [topological_space α] {p : α Prop} :
theorem continuous_subtype_coe {α : Type u} [topological_space α] {p : α Prop} :
theorem continuous.subtype_coe {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α Prop} {f : β subtype p} (hf : continuous f) :
continuous (λ (x : β), (f x))
theorem is_open_map.restrict {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α β} (hf : is_open_map f) {s : set α} (hs : is_open s) :
@[continuity]
theorem continuous.subtype_mk {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α Prop} {f : β α} (h : continuous f) (hp : (x : β), p (f x)) :
continuous (λ (x : β), f x, _⟩)
theorem continuous.subtype_map {α : Type u} {β : Type v} [topological_space α] [topological_space β] {p : α Prop} {f : α β} (h : continuous f) {q : β Prop} (hpq : (x : α), p x q (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 subtype.dense_iff {α : Type u} [topological_space α] {s : set α} {t : set s} :
theorem map_nhds_subtype_coe_eq {α : Type u} [topological_space α] {p : α Prop} {a : α} (ha : p a) (h : {a : α | p a} nhds a) :
filter.map coe (nhds a, ha⟩) = nhds 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 (nhds a) filter.tendsto (λ (x : β), (f x)) b (nhds a)
theorem closure_subtype {α : Type u} [topological_space α] {p : α Prop} {x : {a // p a}} {s : set {a // p a}} :
theorem continuous_at_cod_restrict_iff {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α β} {t : set β} (h1 : (x : α), f x t) {x : α} :
theorem continuous_at.cod_restrict {α : Type u} {β : Type v} [topological_space α] [topological_space β] {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} [topological_space α] [topological_space β] {f : α β} {s : set α} {t : set β} (h1 : set.maps_to f s t) {x : s} (h2 : continuous_at f x) :
theorem continuous_at.restrict_preimage {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α β} {s : set β} {x : (f ⁻¹' s)} (h : continuous_at f x) :
@[continuity]
theorem continuous.cod_restrict {α : Type u} {β : Type v} [topological_space α] [topological_space β] {f : α β} {s : set β} (hf : continuous f) (hs : (a : α), f a s) :
theorem inducing.cod_restrict {α : Type u} {β : Type v} [topological_space α] [topological_space β] {e : α β} (he : inducing e) {s : set β} (hs : (x : α), e x s) :
theorem embedding.cod_restrict {α : Type u} {β : Type v} [topological_space α] [topological_space β] {e : α β} (he : embedding e) (s : set β) (hs : (x : α), e x s) :
theorem embedding_inclusion {α : Type u} [topological_space α] {s t : set α} (h : s t) :
theorem discrete_topology.of_subset {X : Type u_1} [topological_space X] {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 Xon s is discrete, then also the topology induces on t is discrete.

theorem quotient_map_quot_mk {α : Type u} [topological_space α] {r : α α Prop} :
quotient_map (quot.mk r)
@[continuity]
theorem continuous_quot_mk {α : Type u} [topological_space α] {r : α α Prop} :
continuous (quot.mk r)
@[continuity]
theorem continuous_quot_lift {α : Type u} {β : Type v} [topological_space α] [topological_space β] {r : α α Prop} {f : α β} (hr : (a b : α), r a b f a = f b) (h : continuous f) :
continuous (quot.lift f hr)
theorem continuous.quotient_lift {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : setoid α} {f : α β} (h : continuous f) (hs : (a b : α), a b f a = f b) :
theorem continuous.quotient_lift_on' {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : setoid α} {f : α β} (h : continuous f) (hs : (a b : α), setoid.r a b f a = f b) :
continuous (λ (x : quotient s), x.lift_on' f hs)
theorem continuous.quotient_map' {α : Type u} {β : Type v} [topological_space α] [topological_space β] {s : setoid α} {t : setoid β} {f : α β} (hf : continuous f) (H : (setoid.r setoid.r) f f) :
theorem continuous_pi_iff {α : Type u} {ι : Type u_5} {π : ι Type u_6} [topological_space α] [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} :
continuous f (i : ι), continuous (λ (a : α), f a i)
@[continuity]
theorem continuous_pi {α : Type u} {ι : Type u_5} {π : ι Type u_6} [topological_space α] [Π (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 : filter.tendsto f l (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 β} :
filter.tendsto f u (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} [topological_space α] [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} {x : α} :
continuous_at f 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 : filter.tendsto f l (nhds x)) (i : ι) {g : β π i} {xi : π i} (hg : filter.tendsto g l (nhds xi)) :
filter.tendsto (λ (a : β), function.update (f a) i (g a)) l (nhds (function.update x i xi))
theorem continuous_at.update {α : Type u} {ι : Type u_5} {π : ι Type u_6} [topological_space α] [Π (i : ι), topological_space (π i)] {f : α Π (i : ι), π i} [decidable_eq ι] {a : α} (hf : continuous_at f a) (i : ι) {g : α π i} (hg : continuous_at g a) :
continuous_at (λ (a : α), function.update (f a) i (g a)) a
theorem continuous.update {α : Type u} {ι : Type u_5} {π : ι Type u_6} [topological_space α] [Π (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), function.update f.fst 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), pi.single 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), pi.mul_single 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 : filter.tendsto f l (nhds x)) {g : β Π (j : fin n), π ((i.succ_above) j)} {y : Π (j : fin n), π ((i.succ_above) j)} (hg : filter.tendsto g l (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} [topological_space α] {n : } {π : fin (n + 1) Type u_1} [Π (i : fin (n + 1)), topological_space (π i)] (i : fin (n + 1)) {f : α π i} {a : α} (hf : continuous_at f a) {g : α Π (j : fin n), π ((i.succ_above) j)} (hg : continuous_at g a) :
continuous_at (λ (a : α), i.insert_nth (f a) (g a)) a
theorem continuous.fin_insert_nth {α : Type u} [topological_space α] {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)} :
is_open s (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)} :
is_open s (f : Π (a : ι), π a), f s ( (u : Π (a : ι), set (π a)), ( (a : ι), is_open (u a) f a u a) set.univ.pi u 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 σ)} :
is_open s (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 σ)} :
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⟩ = filter.map (sigma.mk i) (nhds x)
theorem sigma.nhds_eq {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] (x : sigma σ) :
theorem comap_sigma_mk_nhds {ι : Type u_5} {σ : ι Type u_7} [Π (i : ι), topological_space (σ i)] (i : ι) (x : σ i) :
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)] [topological_space α] {f : sigma σ α} :
continuous 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)] [topological_space α] {f : sigma σ α} (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)] [topological_space α] {f : sigma σ α} :
is_open_map 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]
@[continuity]
theorem continuous_ulift_up {α : Type u} [topological_space α] :
continuous ulift.up
@[protected, instance]