Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_map.set_of_ideal_of_set_of_is_open

Modification history

2022-10-24 18:38
src/topology/continuous_function/ideals.lean
feat(topology/continuous_function/ideals): maximal ideals correspond to (complements of) singletons (#16719) …
Modified continuous_map.set_of_ideal_of_set_of_is_openView on Github →
2022-10-08 00:38
src/topology/continuous_function/ideals.lean
feat(topology/continuous_function/ideals): construct the Galois correspondence between closed ideals in `C(X, 𝕜)` and open sets in `X` (#16677) …
Added continuous_map.set_of_ideal_of_set_of_is_openView on Github →