to_noetherianSpace

Mathlib.Topology.NoetherianSpace

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.Finite.to_noetherianSpace

English

Finite spaces are Noetherian spaces.

Русский

Конечные пространства являются пространствами Noetherian.

LaTeX

$$$\\text{Finite } \\alpha \\Rightarrow \\text{NoetherianSpace } \\alpha$$$

Lean4

instance (priority := 100) to_noetherianSpace [Finite α] : NoetherianSpace α :=
  ⟨Finite.wellFounded_of_trans_of_irrefl _⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru