Prove2Me

A Noetherian scheme is a Noetherian topological space

Proved
NoetherianScheme.noetherianSpace_of_isNoetherianScheme

by Lucas · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrynoetherian

Let XX be a Noetherian scheme. Then its underlying topological space is a Noetherian topological space: every descending chain of closed subsets

Z1⊇Z2⊇Z3⊇⋯Z_1 \supseteq Z_2 \supseteq Z_3 \supseteq \cdots

is eventually constant (equivalently, every open subset is compact).

Preamble
import Mathlib
import Definitions.Def_NoetherianScheme_defs

universe u

open AlgebraicGeometry NumberField
Formal statement
namespace NoetherianScheme

theorem noetherianSpace_of_isNoetherianScheme (X : Scheme.{u}) (hX : IsNoetherianScheme X) :
    TopologicalSpace.NoetherianSpace X := by sorry

end NoetherianScheme
Source
Wikipedia, "Noetherian scheme", revision 1372079294 (https://en.wikipedia.org/w/index.php?title=Noetherian_scheme&oldid=1372079294), lead section, paragraph 3: "A Noetherian scheme is a Noetherian topological space."
Human review

  • Endorsed by Shuze Chen · Oct 11, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Lucas · Oct 11, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph