2022-04-08 02:06
src/topology/continuous_function/zero_at_infty.lean
feat(topology/continuous_function/zero_at_infty): add more instances for zero_at_infty_continuous_map and establish C₀ functorial properties (#13196) …
Added zero_at_infty_continuous_map.to_bcf_injective