Commit 2022-03-25 19:43 b6d246a6

feat(topology/continuous_function/cocompact_maps): add the type of cocompact continuous maps (#12938) This adds the type of cocompact continuous maps, which are those functions f : α → β for which tendsto f (cocompact α) (cocompact β). These maps are of interest primarily because of their connection with continuous functions vanishing at infinity (#12907). In particular, if f : α → β is a cocompact continuous map and g : β →C₀ γ is a continuous function which vanishes at infinity, then g ∘ f : α →C₀ γ. These are also related to quasi-compact maps (continuous maps for which preimages of compact sets are compact) and proper maps (continuous maps which are universally closed), neither of which are currently defined in mathlib. In particular, quasi-compact maps are cocompact continuous maps, and when the codomain is Hausdorff the converse holds also. Under some additional assumptions, both of these are also equivalent to being a proper map.