set

Mathlib.Topology.NoetherianSpace

URI: https://scilib.ai/kg/mathlib#TopologicalSpace.NoetherianSpace.set

English

A subset s of a Noetherian space α carries the Noetherian property: the subspace s is Noetherian.

Русский

Подпространство s пространства Ноetherian сохраняет свойство Noetherian.

LaTeX

$$$[\\text{NoetherianSpace } \\alpha]\\Rightarrow [\\text{NoetherianSpace } s.Elem].$$$

Lean4

@[stacks 0052 "(1)"]
instance set [NoetherianSpace α] (s : Set α) : NoetherianSpace s :=
  IsInducing.subtypeVal.noetherianSpace

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

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

Разделы

Аффилиация

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