ideal_inf

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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