Continuous bundled map #
In this file we define the type continuous_map
of continuous bundled maps.
- to_fun : α → β
- continuous_to_fun : continuous self.to_fun . "continuity'"
Bundled continuous maps.
Equations
- continuous_map.has_coe_to_fun = {coe := continuous_map.to_fun _inst_2}
Equations
- continuous_map.inhabited = {default := {to_fun := λ (_x : α), default, continuous_to_fun := _}}
The continuous functions from α
to β
are the same as the plain functions when α
is discrete.
The identity as a continuous map.
Equations
- continuous_map.id = {to_fun := id α, continuous_to_fun := _}
The composition of continuous maps, as a continuous map.
Constant map as a continuous map
Equations
- continuous_map.const b = {to_fun := λ (x : α), b, continuous_to_fun := _}
Given two continuous maps f
and g
, this is the continuous map x ↦ (f x, g x)
.
Given two continuous maps f
and g
, this is the continuous map (x, y) ↦ (f x, g y)
.
Abbreviation for product of continuous maps, which is continuous
Equations
- continuous_map.pi f = {to_fun := λ (a : A) (i : I), ⇑(f i) a, continuous_to_fun := _}
The restriction of a continuous function α → β
to a subset s
of α
.
Equations
- continuous_map.restrict s f = {to_fun := ⇑f ∘ coe, continuous_to_fun := _}
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
- continuous_map.lift_cover S φ hφ hS = {to_fun := set.lift_cover S (λ (i : ι), ⇑(φ i)) hφ _, continuous_to_fun := _}
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(α, β)
.
The forward direction of a homeomorphism, as a bundled continuous map.
Equations
- e.to_continuous_map = {to_fun := ⇑e, continuous_to_fun := _}