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
Equations
Equations
- quot.topological_space = topological_space.coinduced (quot.mk r) t
Equations
- sigma.topological_space = ⨆ (a : α), topological_space.coinduced (sigma.mk a) (t₂ a)
Equations
- Pi.topological_space = ⨅ (a : α), topological_space.induced (λ (f : Π (a : α), β a), f a) (t₂ a)
Equations
additive
, multiplicative
#
The topology on those type synonyms is inherited without change.
Equations
- additive.topological_space = _inst_1
Equations
- multiplicative.topological_space = _inst_1
Order dual #
The topology on this type synonym is inherited without change.
Equations
- order_dual.topological_space = _inst_1
The image of a dense set under quotient.mk
is a dense set.
The composition of quotient.mk
and a function with dense range has dense range.
A type synonym equiped with the topology whose open sets are the empty set and the sets with finite complements.
Equations
- cofinite_topology α = α
The identity equivalence between α
and cofinite_topology α
.
Equations
Equations
- cofinite_topology.topological_space = {is_open := λ (s : set (cofinite_topology α)), s.nonempty → sᶜ.finite, is_open_univ := _, is_open_inter := _, is_open_sUnion := _}
Postcomposing f
with prod.fst
is continuous
Precomposing f
with prod.fst
is continuous
Postcomposing f
with prod.fst
is continuous at x
Precomposing f
with prod.fst
is continuous at (x, y)
Precomposing f
with prod.fst
is continuous at x : α × β
Postcomposing f
with prod.snd
is continuous
Precomposing f
with prod.snd
is continuous
Postcomposing f
with prod.snd
is continuous at x
Precomposing f
with prod.snd
is continuous at (x, y)
Precomposing f
with prod.snd
is continuous at x : α × β
A version of continuous_inf_dom_left
for binary functions
A version of continuous_inf_dom_right
for binary functions
A version of continuous_Inf_dom
for binary functions
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.
A product of induced topologies is induced by the product map
prod.fst
maps neighborhood of x : α × β
within the section prod.snd ⁻¹' {x.2}
to 𝓝 x.1
.
The first projection in a product of topological spaces sends open sets to open sets.
prod.snd
maps neighborhood of x : α × β
within the section prod.fst ⁻¹' {x.1}
to 𝓝 x.2
.
The second projection in a product of topological spaces sends open sets to open sets.
The product of two dense sets is a dense set.
If f
and g
are maps with dense range, then prod.map f g
has dense range.
Alias of the reverse direction of continuous_at_cod_restrict_iff
.
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.
function.update f i x
is continuous in (f, x)
.
pi.single i x
is continuous in x
.
pi.mul_single i x
is continuous in 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.
A finite product of discrete spaces is discrete.
A map out of a sum type is continuous iff its restriction to each summand is.
A map out of a sum type is continuous if its restriction to each summand is.