mathlib3

7e0b994c - feat(topology/compact_convergence): define compact convergence (#10967)

feat(topology/compact_convergence): define compact convergence (#10967) And prove that the topology it induces is the compact-open topology Co-authored-by: Chris Birkbeck <cd.birkbeck@gmail.com>