mathlib
9b1f0bb6 - feat(topology/compact_open): convergence in the compact-open topology can be checked on compact sets (#9240)
