ofIdeals_ideal

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_ideal

English

For any ideal data I on X, applying ofIdeals to I.ideal recovers I.

Русский

Для любого набора идеалов I на X применение ofIdeals к I.ideal восстанавливает I.

LaTeX

$$$ \operatorname{ofIdeals}(I.ideal) = I $$$

Lean4

theorem ofIdeals_ideal (I : IdealSheafData X) : ofIdeals I.ideal = I :=
  IdealSheafData.gci.u_l_eq _

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

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

Разделы

Аффилиация

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