English
If α is Noetherian and f: α → β is continuous, then the range of f is a Noetherian space (as a subspace of β).
Русский
Если α Ноetherian и f непрерывно отображает в β, то образ f — это подпространство β, которое также Ноetherian.
LaTeX
$$$[\\text{NoetherianSpace } \\alpha]\\;\\Rightarrow\\; [\\text{NoetherianSpace } (\\mathrm{Set.range}(f)).\\Elem]$$$
Lean4
theorem noetherianSpace_TFAE :
TFAE
[NoetherianSpace α, WellFoundedLT (Closeds α), ∀ s : Set α, IsCompact s, ∀ s : Opens α, IsCompact (s : Set α)] :=
by
tfae_have 1 ↔ 2 := by
simp_rw [isWellFounded_iff]
exact Opens.compl_bijective.2.wellFounded_iff (@OrderIso.compl (Set α)).lt_iff_lt.symm
tfae_have 1 ↔ 4 := noetherianSpace_iff_opens α
tfae_have 1 → 3 := @NoetherianSpace.isCompact α _
tfae_have 3 → 4 := fun h s => h s
tfae_finish
