Theorem continuous_map.set_of_top_eq_univ

feat(topology/continuous_function/ideals): construct the Galois correspondence between closed ideals in `C(X, 𝕜)` and open sets in `X` (#16677) …