English
For a space α, the following four conditions are equivalent: α is Noetherian, the closed sets are well-founded by inclusion, every subset is compact, and every open set is compact.
Русский
Для пространства α эквивалентны следующие четыре условия: α- пространство Неферова, множество замкнутых множеств хорошо упорядочено по включению, каждоe подмножество компактно, и каждоe открытое множество компактно.
LaTeX
$$$\\text{TFAE} [\\text{NoetherianSpace } \\alpha,\\; \\text{WellFoundedLT}(\\text{Closeds } \\alpha),\\; \\forall s \\subseteq \\alpha, \\text{IsCompact } s,\\; \\forall s \\in \\text{Opens}(\\alpha), \\text{IsCompact}(s)].$$$
Lean4
/-- Type class for Noetherian spaces. It is defined to be spaces whose open sets satisfies ACC. -/
abbrev NoetherianSpace : Prop :=
WellFoundedGT (Opens α)
