noetherian_univ_iff — Mathlib

English

Noetherian property of the whole space is equivalent to the Noetherian property of the universal set.

Русский

Свойство Ноetherian для всего пространства эквивалентно свойству Ноetherian для множества единицы $Set.univ$.

LaTeX

$$$\\text{noetherian_univ_iff} : NoetherianSpace(\\text{Set.univ} : Set\\,\\alpha) \\iff NoetherianSpace \\alpha$$$

Lean4

@[simp]
theorem noetherian_univ_iff : NoetherianSpace (Set.univ : Set α) ↔ NoetherianSpace α :=
  noetherianSpace_iff_of_homeomorph (Homeomorph.Set.univ α)

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