mathlib documentation

topology.noetherian_space

Noetherian space #

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 topological_space.noetherian_space_tfae.

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 #

@[class]
structure topological_space.noetherian_space (α : Type u_1) [topological_space α] :
Prop

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.