mathlib documentation


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 #

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
theorem topological_space.noetherian_space.Union {α : Type u_1} [topological_space α] {ι : Type u_2} (f : ι → set α) [finite ι] [hf : ∀ (i : ι), topological_space.noetherian_space (f i)] :

Spaces that are both Noetherian and Hausdorff is finite.