Noetherian space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
A Noetherian space is a topological space that satisfies any of the following equivalent conditions:
The first is chosen as the definition, and the equivalence is shown in
Many examples of noetherian spaces come from algebraic topology. For example, the underlying space
of a noetherian scheme (e.g., the spectrum of a noetherian ring) is noetherian.
Main Results #
noetherian_space.set: Every subspace of a noetherian space is noetherian.
noetherian_space.is_compact: Every subspace of a noetherian space is compact.
noetherian_space_tfae: Describes the equivalent definitions of noetherian spaces.
noetherian_space.range: The image of a noetherian space under a continuous map is noetherian.
noetherian_space.Union: The finite union of noetherian spaces is noetherian.
noetherian_space.discrete: A noetherian and hausdorff space is discrete.
noetherian_space.exists_finset_irreducible : Every closed subset of a noetherian space is a
finite union of irreducible closed subsets.
noetherian_space.finite_irreducible_components: The number of irreducible components of a
noetherian space is finite.
Type class for noetherian spaces. It is defined to be spaces whose open sets satisfies ACC.
Instances of this typeclass
Spaces that are both Noetherian and Hausdorff is finite.