Continuous bundled maps #
In this file we define the type continuous_map
of continuous bundled maps.
We use the fun_like
design, so each type of morphisms has a companion typeclass which is meant to
be satisfied by itself and all stricter types.
- to_fun : α → β
- continuous_to_fun : continuous self.to_fun . "continuity'"
The type of continuous maps from α
to β
.
When possible, instead of parametrizing results over (f : C(α, β))
,
you should parametrize over {F : Type*} [continuous_map_class F α β] (f : F)
.
When you extend this structure, make sure to extend continuous_map_class
.
Instances for continuous_map
- continuous_map.has_abs
- continuous_map.has_sizeof_inst
- continuous_map.has_coe_t
- continuous_map.continuous_map_class
- continuous_map.has_coe_to_fun
- continuous_map.inhabited
- continuous_map.nontrivial
- homeomorph.continuous_map.has_coe
- continuous_map.compact_open
- continuous_map.t2_space
- nnreal.continuous_map.can_lift
- Top.bundled_hom
- continuous_map.partial_order
- continuous_map.has_sup
- continuous_map.semilattice_sup
- continuous_map.has_inf
- continuous_map.semilattice_inf
- continuous_map.lattice
- continuous_map.compact_convergence_uniform_space
- continuous_map.has_mul
- continuous_map.has_add
- continuous_map.has_one
- continuous_map.has_zero
- continuous_map.has_nat_cast
- continuous_map.has_int_cast
- continuous_map.has_nsmul
- continuous_map.has_pow
- continuous_map.has_inv
- continuous_map.has_neg
- continuous_map.has_div
- continuous_map.has_sub
- continuous_map.has_zsmul
- continuous_map.has_zpow
- continuous_map.semigroup
- continuous_map.add_semigroup
- continuous_map.comm_semigroup
- continuous_map.add_comm_semigroup
- continuous_map.mul_one_class
- continuous_map.add_zero_class
- continuous_map.mul_zero_class
- continuous_map.semigroup_with_zero
- continuous_map.monoid
- continuous_map.add_monoid
- continuous_map.monoid_with_zero
- continuous_map.comm_monoid
- continuous_map.add_comm_monoid
- continuous_map.comm_monoid_with_zero
- continuous_map.has_continuous_mul
- continuous_map.has_continuous_add
- continuous_map.group
- continuous_map.add_group
- continuous_map.comm_group
- continuous_map.add_comm_group
- continuous_map.topological_group
- continuous_map.topological_add_group
- continuous_map.non_unital_non_assoc_semiring
- continuous_map.non_unital_semiring
- continuous_map.add_monoid_with_one
- continuous_map.non_assoc_semiring
- continuous_map.semiring
- continuous_map.non_unital_non_assoc_ring
- continuous_map.non_unital_ring
- continuous_map.non_assoc_ring
- continuous_map.ring
- continuous_map.non_unital_comm_semiring
- continuous_map.comm_semiring
- continuous_map.non_unital_comm_ring
- continuous_map.comm_ring
- continuous_map.has_smul
- continuous_map.has_vadd
- continuous_map.has_continuous_const_smul
- continuous_map.has_continuous_const_vadd
- continuous_map.has_continuous_smul
- continuous_map.has_continuous_vadd
- continuous_map.smul_comm_class
- continuous_map.vadd_comm_class
- continuous_map.is_scalar_tower
- continuous_map.is_central_scalar
- continuous_map.mul_action
- continuous_map.distrib_mul_action
- continuous_map.module
- continuous_map.algebra
- continuous_map.has_smul'
- continuous_map.module'
- continuous_map.has_star
- continuous_map.has_involutive_star
- continuous_map.star_add_monoid
- continuous_map.star_semigroup
- continuous_map.star_ring
- continuous_map.star_module
- continuous_map.metric_space
- continuous_map.complete_space
- continuous_map.has_norm
- continuous_map.normed_add_comm_group
- continuous_map.normed_ring
- continuous_map.normed_space
- continuous_map.normed_algebra
- continuous_map.normed_star_group
- continuous_map.cstar_ring
- continuous_affine_map.continuous_map.has_coe
- cont_mdiff_map.continuous_map.has_coe
- locally_constant.continuous_map.has_coe
- continuous_map.can_lift
- coe : F → Π (a : α), (λ (_x : α), β) a
- coe_injective' : function.injective continuous_map_class.coe
- map_continuous : ∀ (f : F), continuous ⇑f
continuous_map_class F α β
states that F
is a type of continuous maps.
You should extend this class when you extend continuous_map
.
Instances of this typeclass
- continuous_semilinear_map_class.to_continuous_map_class
- spectral_map_class.to_continuous_map_class
- continuous_map.homotopy_like.to_continuous_map_class
- bounded_continuous_map_class.to_continuous_map_class
- continuous_monoid_hom_class.to_continuous_map_class
- continuous_add_monoid_hom_class.to_continuous_map_class
- cocompact_map_class.to_continuous_map_class
- zero_at_infty_continuous_map_class.to_continuous_map_class
- continuous_open_map_class.to_continuous_map_class
- continuous_order_hom_class.to_continuous_map_class
- continuous_map.continuous_map_class
Instances of other typeclasses for continuous_map_class
- continuous_map_class.has_sizeof_inst
Equations
- continuous_map.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, continuous_to_fun := _}}
Continuous maps #
Equations
- continuous_map.continuous_map_class = {coe := continuous_map.to_fun _inst_2, coe_injective' := _, map_continuous := _}
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Copy of a continuous_map
with a new to_fun
equal to the old one. Useful to fix definitional
equalities.
Equations
- f.copy f' h = {to_fun := f', continuous_to_fun := _}
Deprecated. Use map_continuous
instead.
Deprecated. Use map_continuous_at
instead.
Deprecated. Use fun_like.congr_fun
instead.
Deprecated. Use fun_like.congr_arg
instead.
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 constant map as a continuous map.
Equations
- continuous_map.const α b = {to_fun := function.const α b, continuous_to_fun := _}
Equations
The composition of continuous maps, as a continuous map.
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 := _}
The restriction of a continuous map onto the preimage of a set.
Equations
- f.restrict_preimage s = {to_fun := s.restrict_preimage ⇑f, 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 := _}
homeomorph.to_continuous_map
as a coercion.
Equations
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
.