2022-04-06 06:48
src/topology/continuous_function/zero_at_infty.lean
feat(topology/continuous_function/zero_at_infty): add the type of continuous functions vanishing at infinity (#12907) …
Added zero_at_infty_continuous_map.zero_at_infty_continuous_map_class.of_compact