noetherianSpace_iff_opens — Mathlib

English

Noetherian space α is equivalent to every open set being compact.

Русский

Пространство Ноетеря α эквивалентно тому, что каждое открытое множество компактно.

LaTeX

$$$\\text{NoetherianSpace } \\alpha \\iff \\forall s:\\text{Opens }(\\alpha),\\; IsCompact(s : Set\\alpha).$$$

Lean4

theorem noetherianSpace_iff_opens : NoetherianSpace α ↔ ∀ s : Opens α, IsCompact (s : Set α) :=
  by
  rw [NoetherianSpace, CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact,
    CompleteLattice.isSupFiniteCompact_iff_all_elements_compact]
  exact forall_congr' Opens.isCompactElement_iff

Похожие утверждения