coe_support

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

The coe projection from the Simps simp namespace equals the defined support.

Русский

Проекция из пространства Simps совпадает с данной поддержкой.

LaTeX

$$coe_support(I) = I.support$$

Lean4

/-- Custom simps projection for `IdealSheafData`. -/
def coe_support : Set X :=
  I.support

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

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

Разделы

Аффилиация

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