Commit 2026-02-10 22:14 c2b78d26
View on Github →feat(Topology/Irreducible): union of irreducible components (#34421) This PR adds a few API lemmas on unions of irreducible components. @alreadydone pointed out that this then gives a nice golf of TopologicalSpace.NoetherianSpace.exists_isOpen_nonempty_subset_irreducibleComponent