mathlib3

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

feat(topology/continuous_function/ideals): construct the Galois correspondence between closed ideals in `C(X, 𝕜)` and open sets in `X` (#16677) For a topological ring `R` and a topological space `X` there is a Galois connection between `ideal C(X, R)` and `set X` given by sending each `I : ideal C(X, R)` to `{x : X | ∀ f ∈ I, f x = 0}ᶜ` and mapping `s : set X` to the ideal with carrier `{f : C(X, R) | ∀ x ∈ sᶜ, f x = 0}`, and we call these maps `continuous_map.set_of_ideal` and `continuous_map.ideal_of_set`. As long as `R` is Hausdorff, `continuous_map.set_of_ideal I` is open, and if, in addition, `X` is locally compact, then `continuous_map.set_of_ideal s` is closed.