Continuous affine maps. #
This file defines a type of bundled continuous affine maps.
Note that the definition and basic properties established here require minimal assumptions, and do not even assume compatibility between the topological and algebraic structures. Of course it is necessary to assume some compatibility in order to obtain a useful theory. Such a theory is developed elsewhere for affine spaces modelled on normed vector spaces, but not yet for general topological affine spaces (since we have not defined these yet).
Main definitions: #
Notation: #
We introduce the notation P →A[R] Q
for ContinuousAffineMap R P Q
. Note that this is parallel
to the notation E →L[R] F
for ContinuousLinearMap R E F
.
- toFun : P → Q
- map_vadd' : ∀ (p : P) (v : V), AffineMap.toFun s.toAffineMap (v +ᵥ p) = ↑s.linear v +ᵥ AffineMap.toFun s.toAffineMap p
- cont : Continuous s.toFun
A continuous map of affine spaces.
Instances For
Helper instance for when there's too many metavariables to apply
FunLike.hasCoeToFun
directly.
Forgetting its algebraic properties, a continuous affine map is a continuous map.
Instances For
The constant map is a continuous affine map.
Instances For
The composition of morphisms is a morphism.
Instances For
A continuous linear map can be regarded as a continuous affine map.