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]
Equations
@[protected, instance]
def
quot.topological_space
{α : Type u}
{r : α → α → Prop}
[t : topological_space α] :
topological_space (quot r)
Equations
- quot.topological_space = topological_space.coinduced (quot.mk r) t
@[protected, instance]
@[protected, instance]
def
prod.topological_space
{α : Type u}
{β : Type v}
[t₁ : topological_space α]
[t₂ : topological_space β] :
topological_space (α × β)
@[protected, instance]
def
sum.topological_space
{α : Type u}
{β : Type v}
[t₁ : topological_space α]
[t₂ : topological_space β] :
topological_space (α ⊕ β)
@[protected, instance]
def
sigma.topological_space
{α : Type u}
{β : α → Type v}
[t₂ : Π (a : α), topological_space (β a)] :
Equations
- sigma.topological_space = ⨆ (a : α), topological_space.coinduced (sigma.mk a) (t₂ a)
@[protected, instance]
def
Pi.topological_space
{α : Type u}
{β : α → Type v}
[t₂ : Π (a : α), topological_space (β a)] :
topological_space (Π (a : α), β a)
Equations
- Pi.topological_space = ⨅ (a : α), topological_space.induced (λ (f : Π (a : α), β a), f a) (t₂ a)
@[protected, instance]
Equations
additive, multiplicative #
The topology on those type synonyms is inherited without change.
@[protected, instance]
Equations
- additive.topological_space = _inst_1
@[protected, instance]
Equations
- multiplicative.topological_space = _inst_1
@[protected, instance]
@[protected, instance]
theorem
nhds_of_mul
{α : Type u}
[topological_space α]
(a : α) :
nhds (⇑additive.of_mul a) = filter.map ⇑additive.of_mul (nhds a)
theorem
nhds_to_mul
{α : Type u}
[topological_space α]
(a : additive α) :
nhds (⇑additive.to_mul a) = filter.map ⇑additive.to_mul (nhds a)
Order dual #
The topology on this type synonym is inherited without change.
@[protected, instance]
Equations
- order_dual.topological_space = _inst_1
@[protected, instance]
theorem
quotient.preimage_mem_nhds
{α : Type u}
[topological_space α]
[s : setoid α]
{V : set (quotient s)}
{a : α}
(hs : V ∈ nhds ⟦a⟧) :
quotient.mk ⁻¹' V ∈ nhds a
theorem
dense.quotient
{α : Type u}
[setoid α]
[topological_space α]
{s : set α}
(H : dense s) :
dense (quotient.mk '' 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) :
dense_range (quotient.mk ∘ 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}
[topological_space α]
[discrete_topology α] :
@[protected, instance]
def
sum.discrete_topology
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[hα : discrete_topology α]
[hβ : discrete_topology β] :
discrete_topology (α ⊕ β)
@[protected, instance]
def
sigma.discrete_topology
{α : Type u}
{β : α → Type v}
[Π (a : α), topological_space (β a)]
[h : ∀ (a : α), discrete_topology (β a)] :
theorem
nhds_within_subtype_eq_bot_iff
{α : Type u}
[topological_space α]
{s t : set α}
{x : ↥s} :
nhds_within x (coe ⁻¹' t) = ⊥ ↔ nhds_within ↑x t ⊓ filter.principal s = ⊥
theorem
nhds_ne_subtype_eq_bot_iff
{α : Type u}
[topological_space α]
{S : set α}
{x : ↥S} :
nhds_within x {x}ᶜ = ⊥ ↔ nhds_within ↑x {↑x}ᶜ ⊓ filter.principal S = ⊥
theorem
nhds_ne_subtype_ne_bot_iff
{α : Type u}
[topological_space α]
{S : set α}
{x : ↥S} :
(nhds_within x {x}ᶜ).ne_bot ↔ (nhds_within ↑x {↑x}ᶜ ⊓ filter.principal S).ne_bot
theorem
discrete_topology_subtype_iff
{α : Type u}
[topological_space α]
{S : set α} :
discrete_topology ↥S ↔ ∀ (x : α), x ∈ S → nhds_within x {x}ᶜ ⊓ filter.principal S = ⊥
A type synonym equiped with the topology whose open sets are the empty set and the sets with finite complements.
Equations
- cofinite_topology α = α
Instances for cofinite_topology
The identity equivalence between α and cofinite_topology α.
Equations
@[protected, instance]
@[protected, instance]
Equations
- cofinite_topology.topological_space = {is_open := λ (s : set (cofinite_topology α)), s.nonempty → sᶜ.finite, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
theorem
cofinite_topology.mem_nhds_iff
{α : Type u}
{a : cofinite_topology α}
{s : set (cofinite_topology α)} :
@[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
continuous_uncurry_left
{α : Type u}
{β : Type v}
{γ : Type u_1}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → β → γ}
(a : α)
(h : continuous (function.uncurry f)) :
continuous (f a)
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) :
continuous (function.curry g a)
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 : β} :
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
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)
@[protected, instance]
def
prod.discrete_topology
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
[discrete_topology α]
[discrete_topology β] :
discrete_topology (α × β)
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) :
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
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_eq_generate_from
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β] :
theorem
prod_induced_induced
{β : Type v}
{δ : Type u_2}
[topological_space β]
[topological_space δ]
{α : Type u_1}
{γ : Type u_3}
(f : α → β)
(g : γ → δ) :
prod.topological_space = topological_space.induced (λ (p : α × γ), (f p.fst, g p.snd)) prod.topological_space
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
map_fst_nhds_within
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(x : α × β) :
filter.map prod.fst (nhds_within x (prod.snd ⁻¹' {x.snd})) = nhds x.fst
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 : α × β) :
filter.map prod.snd (nhds_within x (prod.fst ⁻¹' {x.fst})) = nhds x.snd
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
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 β) :
@[simp]
theorem
frontier_prod_univ_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(s : set α) :
@[simp]
theorem
frontier_univ_prod_eq
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
(s : set β) :
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) :
theorem
is_closed.prod
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s₁ : set α}
{s₂ : set β}
(h₁ : is_closed s₁)
(h₂ : is_closed s₂) :
theorem
dense.prod
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{s : set α}
{t : set β}
(hs : dense s)
(ht : dense 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) :
dense_range (prod.map f g)
If f and g are maps with dense range, then prod.map f g has dense range.
theorem
inducing.prod_mk
{α : Type u}
{β : Type v}
{γ : Type u_1}
{δ : Type u_2}
[topological_space α]
[topological_space β]
[topological_space γ]
[topological_space δ]
{f : α → β}
{g : γ → δ}
(hf : inducing f)
(hg : inducing g) :
@[simp]
theorem
inducing_const_prod
{α : Type u}
{β : Type v}
{γ : Type u_1}
[topological_space α]
[topological_space β]
[topological_space γ]
{a : α}
{f : β → γ} :
@[simp]
theorem
inducing_prod_const
{α : Type u}
{β : Type v}
{γ : Type u_1}
[topological_space α]
[topological_space β]
[topological_space γ]
{b : β}
{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) :
@[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
closed_embedding_inl
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β] :
theorem
closed_embedding_inr
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β] :
theorem
continuous_sum_dom
{α : Type u}
{β : Type v}
{γ : Type u_1}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α ⊕ β → γ} :
continuous f ↔ continuous (f ∘ sum.inl) ∧ continuous (f ∘ sum.inr)
theorem
continuous_sum_elim
{α : Type u}
{β : Type v}
{γ : Type u_1}
[topological_space α]
[topological_space β]
[topological_space γ]
{f : α → γ}
{g : β → γ} :
continuous (sum.elim f g) ↔ continuous f ∧ continuous 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) :
continuous (sum.elim f 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 : γ → δ} :
continuous (sum.map f g) ↔ continuous f ∧ continuous 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) :
continuous (sum.map f 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 : β → γ} :
is_open_map (sum.elim f g) ↔ is_open_map f ∧ is_open_map 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) :
is_open_map (sum.elim f g)
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)) :
inducing f
theorem
closed_embedding_subtype_coe
{α : Type u}
[topological_space α]
{p : α → Prop}
(h : is_closed {a : α | p a}) :
@[continuity]
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.open_embedding_subtype_coe
{α : Type u}
[topological_space α]
{s : set α}
(hs : is_open s) :
theorem
is_open.is_open_map_subtype_coe
{α : Type u}
[topological_space α]
{s : set α}
(hs : is_open s) :
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) :
is_open_map (s.restrict f)
theorem
is_closed.closed_embedding_subtype_coe
{α : Type u}
[topological_space α]
{s : set α}
(hs : is_closed 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)) :
continuous (subtype.map f hpq)
theorem
continuous_at_subtype_coe
{α : Type u}
[topological_space α]
{p : α → Prop}
{a : subtype p} :
theorem
map_nhds_subtype_coe_eq
{α : Type u}
[topological_space α]
{p : α → Prop}
{a : α}
(ha : p a)
(h : {a : α | p a} ∈ nhds 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
continuous_at_cod_restrict_iff
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
{t : set β}
(h1 : ∀ (x : α), f x ∈ t)
{x : α} :
continuous_at (set.cod_restrict f t h1) x ↔ continuous_at f x
theorem
continuous_at.cod_restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{f : α → β}
{t : set β}
(h1 : ∀ (x : α), f x ∈ t)
{x : α} :
continuous_at f x → continuous_at (set.cod_restrict f t h1) 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) :
continuous_at (set.maps_to.restrict f s t h1) 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) :
continuous_at (s.restrict_preimage 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) :
continuous (set.cod_restrict f s hs)
theorem
inducing.cod_restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{e : α → β}
(he : inducing e)
{s : set β}
(hs : ∀ (x : α), e x ∈ s) :
inducing (set.cod_restrict e s hs)
theorem
embedding.cod_restrict
{α : Type u}
{β : Type v}
[topological_space α]
[topological_space β]
{e : α → β}
(he : embedding e)
(s : set β)
(hs : ∀ (x : α), e x ∈ s) :
embedding (set.cod_restrict e s hs)
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) :
continuous (quotient.lift f hs)
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) :
continuous (quotient.map' f H)
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
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
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 : ι} :
continuous (sigma.mk i)
theorem
is_open_map_sigma_mk
{ι : Type u_5}
{σ : ι → Type u_7}
[Π (i : ι), topological_space (σ i)]
{i : ι} :
is_open_map (sigma.mk 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) :
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) :
@[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₁) :
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₁) :
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]
@[protected, instance]