Locally bounded maps #
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 #
locally_bounded_map
: Locally bounded maps. Maps which preserve boundedness.
Typeclasses #
- to_fun : α → β
- comap_cobounded_le' : filter.comap self.to_fun (bornology.cobounded β) ≤ bornology.cobounded α
The type of bounded maps from α
to β
, the maps which send a bounded set to a bounded set.
Instances for locally_bounded_map
- to_fun_like : fun_like F α (λ (_x : α), β)
- comap_cobounded_le : ∀ (f : F), filter.comap ⇑f (bornology.cobounded β) ≤ bornology.cobounded α
locally_bounded_map_class F α β
states that F
is a type of bounded maps.
You should extend this class when you extend locally_bounded_map
.
Instances of this typeclass
Instances of other typeclasses for locally_bounded_map_class
- locally_bounded_map_class.has_sizeof_inst
Equations
- locally_bounded_map.has_coe_t = {coe := λ (f : F), {to_fun := ⇑f, comap_cobounded_le' := _}}
Equations
- locally_bounded_map.locally_bounded_map_class = {to_fun_like := {coe := λ (f : locally_bounded_map α β), f.to_fun, coe_injective' := _}, comap_cobounded_le := _}
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Copy of a locally_bounded_map
with a new to_fun
equal to the old one. Useful to fix
definitional equalities.
Equations
- f.copy f' h = {to_fun := f', comap_cobounded_le' := _}
Construct a locally_bounded_map
from the fact that the function maps bounded sets to bounded
sets.
Equations
- locally_bounded_map.of_map_bounded f h = {to_fun := f, comap_cobounded_le' := _}
id
as a locally_bounded_map
.
Equations
- locally_bounded_map.id α = {to_fun := id α, comap_cobounded_le' := _}
Equations
- locally_bounded_map.inhabited α = {default := locally_bounded_map.id α _inst_1}
Composition of locally_bounded_map
s as a locally_bounded_map
.