Locally bounded maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines locally bounded maps between bornologies.
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.
Types of morphisms #
The type of bounded maps from
β, the maps which send a bounded set to a bounded set.
locally_bounded_map_class F α β states that
F is a type of bounded maps.
You should extend this class when you extend
Instances of this typeclass
Instances of other typeclasses for
Helper instance for when there's too many metavariables to apply
Copy of a
locally_bounded_map with a new
to_fun equal to the old one. Useful to fix
locally_bounded_map from the fact that the function maps bounded sets to bounded