Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-16 08:21 91f98e82

View on Github →

feat(topology/bornology/hom): Locally bounded maps (#12046) Define locally_bounded_map, the type of locally bounded maps between two bornologies.

Estimated changes

Modified src/topology/bornology/basic.lean

added theorem bornology.comap_cobounded_le_iff

modified theorem bornology.is_bounded_compl_iff

modified theorem bornology.is_bounded_empty

added theorem bornology.is_cobounded_compl_iff

Created src/topology/bornology/hom.lean

added theorem is_bounded.image

added theorem locally_bounded_map.cancel_left

added theorem locally_bounded_map.cancel_right

added theorem locally_bounded_map.coe_comp

added theorem locally_bounded_map.coe_id

added theorem locally_bounded_map.coe_of_map_bounded

added def locally_bounded_map.comp

added theorem locally_bounded_map.comp_apply

added theorem locally_bounded_map.comp_assoc

added theorem locally_bounded_map.comp_id

added theorem locally_bounded_map.ext

added theorem locally_bounded_map.id_apply

added theorem locally_bounded_map.id_comp

added def locally_bounded_map.of_map_bounded

added theorem locally_bounded_map.of_map_bounded_apply

added theorem locally_bounded_map.to_fun_eq_coe

added structure locally_bounded_map