mathlib3

7e20c8fc - feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies (#15721)

feat(topology): composition of continuous functions is continuous w.r.t. the compact-open topologies (#15721) * Remove the `t2_space` assumption from `exists_compact_between` by generalizing the proof of `exists_compact_superset`, and move it from `topology/separation` to `topology/subset_properties`. * Use it to prove `continuous_map.continuous_prod` in `topology/continuous_map` stating that for topological spaces `X,Y,Z` with `Y` locally compact, the composition induces a continuous map from `C(X,Y) x C(Y,Z)` to `C(X,Z)` where all function spaces are endowed with the compact-open topology. The (statement and the) proof is taken from Prop. 9 of Chap. X, §3, №. 4 of Bourbaki's *Topologie Générale*. * Generalize `exists_open_between_and_is_compact_closure` from `t3_space` to `t2_space` using the generalized `exists_compact_between`. This has been briefly discussed in [this Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/continuity.20of.20continuous.20composition) Co-authored-by: Oliver Nash <github@olivernash.org>