mathlib3 documentation


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 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 #

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

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.