OAI/GroupTheory/PolycyclicRecognition/Algebra/NoetherianComponents.lean
2 declarations, 0 contain sorry, 0 declared as axioms
Finitely many connected components in a Noetherian space
Each irreducible component lies in one connected component, and every point lies in an irreducible component. The finite irreducible-component cover therefore gives finitely many connected components.
- theorem
OAI.PolycyclicRecognition.finite_connectedComponents_of_noetherianline 18 - theorem
OAI.PolycyclicRecognition.isOpen_connectedComponent_of_noetherianline 35