Commit 2022-08-29 16:05 7e20c8fc

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