ideal_sup

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

The ideal of the join of two ideal sheaf data equals the join of their ideals, computed pointwise.

Русский

Идеал сложения двух данных идеалов равен сложению их идеалов, считаемому по точкам.

LaTeX

$$$ (I \lor J).ideal = I.ideal \lor J.ideal $$$

Lean4

@[simp]
theorem ideal_sup {I J : IdealSheafData X} : (I ⊔ J).ideal = I.ideal ⊔ J.ideal :=
  rfl

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

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

Разделы

Аффилиация

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