https://github.com/math-comp/analysis/blob/c6942fdeb9dd7bcd94ae6ed80c3f74703d48f436/theories/topology_theory/topology_structure.v#L1039 because `cts_fun` is difficult to `Search` @mkerjean
