ideal_sSup

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

The ideal of the supremum of a set of ideal data equals the supremum of the images of their ideals.

Русский

Идеал сверху множества данных идеалов равен супремуму их образов через идеалы.

LaTeX

$$$ (\mathrm{sSup} I).ideal = \mathrm{sSup}(\mathrm{ideal} \!''\! I) $$$

Lean4

@[simp]
theorem ideal_sSup {I : Set (IdealSheafData X)} : (sSup I).ideal = sSup (ideal '' I) :=
  rfl

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

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

Разделы

Аффилиация

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