Continuous bundled maps #
In this file we define the type ContinuousMap
of continuous bundled maps.
We use the DFunLike
design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
Continuous maps #
Deprecated. Use map_continuousAt
instead.
The continuous functions from α
to β
are the same as the plain functions when α
is discrete.
Equations
Instances For
The identity as a continuous map.
Equations
Instances For
The constant map as a continuous map.
Equations
Instances For
Equations
The composition of continuous maps, as a continuous map.
Equations
Instances For
Prod.fst : (x, y) ↦ x
as a bundled continuous map.
Equations
Instances For
Prod.snd : (x, y) ↦ y
as a bundled continuous map.
Equations
Instances For
Given two continuous maps f
and g
, this is the continuous map x ↦ (f x, g x)
.
Equations
Instances For
Given two continuous maps f
and g
, this is the continuous map (x, y) ↦ (f x, g y)
.
Equations
Instances For
Prod.swap
bundled as a ContinuousMap
.
Equations
Instances For
Sigma.mk i
as a bundled continuous map.
Equations
Instances For
To give a continuous map out of a disjoint union, it suffices to give a continuous map out of
each term. This is Sigma.uncurry
for continuous maps.
Equations
Instances For
Giving a continuous map out of a disjoint union is the same as giving a continuous map out of
each term. This is a version of Equiv.piCurry
for continuous maps.
Equations
Instances For
Abbreviation for product of continuous maps, which is continuous
Equations
Instances For
Evaluation at point as a bundled continuous map.
Equations
Instances For
Giving a continuous map out of a disjoint union is the same as giving a continuous map out of each term
Equations
Instances For
Combine a collection of bundled continuous maps C(X i, Y i)
into a bundled continuous map
C(∀ i, X i, ∀ i, Y i)
.
Equations
Instances For
"Precomposition" as a continuous map between dependent types.
Equations
Instances For
The restriction of a continuous function α → β
to a subset s
of α
.
Equations
Instances For
The restriction of a continuous map to the preimage of a set.
Equations
Instances For
A family φ i
of continuous maps C(S i, β)
, where the domains S i
contain a neighbourhood
of each point in α
and the functions φ i
agree pairwise on intersections, can be glued to
construct a continuous map in C(α, β)
.
Equations
Instances For
A family F s
of continuous maps C(s, β)
, where (1) the domains s
are taken from a set A
of sets in α
which contain a neighbourhood of each point in α
and (2) the functions F s
agree
pairwise on intersections, can be glued to construct a continuous map in C(α, β)
.
Equations
Instances For
Set.inclusion
as a bundled continuous map.
Equations
Instances For
Setoid.quotientKerEquivOfRightInverse
as a homeomorphism.
Equations
Instances For
The homeomorphism from the quotient of a quotient map to its codomain. This is
Setoid.quotientKerEquivOfSurjective
as a homeomorphism.
Equations
Instances For
Descend a continuous map, which is constant on the fibres, along a quotient map.
Equations
Instances For
The obvious triangle induced by IsQuotientMap.lift
commutes:
g
X --→ Z
| ↗
f | / hf.lift g h
v /
Y
IsQuotientMap.lift
as an equivalence.
Equations
Instances For
Left inverse to a continuous map from a homeomorphism, mirroring Equiv.symm_comp_self
.
Right inverse to a continuous map from a homeomorphism, mirroring Equiv.self_comp_symm
.