mathlib

6d94ff7b - feat(topology/subset_properties, noetherian_space): Noetherian spaces have finite irreducible components. (#17015)

feat(topology/subset_properties, noetherian_space): Noetherian spaces have finite irreducible components. (#17015) The previous statement was too weak. Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>