Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-08 00:38 54f74fc8

View on Github โ†’

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.

Estimated changes