Locally bounded maps #
This file defines locally bounded maps between bornologies.
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.
Types of morphisms #
LocallyBoundedMap
: Locally bounded maps. Maps which preserve boundedness.
Typeclasses #
The type of bounded maps from α
to β
, the maps which send a bounded set to a bounded set.
- toFun : α → β
The function underlying a locally bounded map
The pullback of the
Bornology.cobounded
filter under the function is contained in the cobounded filter. Equivalently, the function maps bounded sets to bounded sets.
Instances For
LocallyBoundedMapClass F α β
states that F
is a type of bounded maps.
You should extend this class when you extend LocallyBoundedMap
.
The pullback of the
Bornology.cobounded
filter under the function is contained in the cobounded filter. Equivalently, the function maps bounded sets to bounded sets.
Instances
Turn an element of a type F
satisfying LocallyBoundedMapClass F α β
into an actual
LocallyBoundedMap
. This is declared as the default coercion from F
to
LocallyBoundedMap α β
.
Equations
Instances For
Equations
Equations
Copy of a LocallyBoundedMap
with a new toFun
equal to the old one. Useful to fix
definitional equalities.
Equations
Instances For
Construct a LocallyBoundedMap
from the fact that the function maps bounded sets to bounded
sets.
Equations
Instances For
Equations
Composition of LocallyBoundedMap
s as a LocallyBoundedMap
.