ideal_ofIdeals_le

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

For any family I of ideals, the ideal part of the object ofIdeals(I) is below I, i.e. (ofIdeals I).ideal ≤ I.

Русский

Для любойFamily I из Ideals выполняется: (ofIdeals(I)).ideal ≤ I.

LaTeX

$$$(\operatorname{ofIdeals}(I)).\mathrm{ideal}(U) \le I(U) \quad \text{for all } U$$$

Lean4

theorem ideal_ofIdeals_le (I : ∀ U : X.affineOpens, Ideal Γ(X, U)) : (ofIdeals I).ideal ≤ I :=
  sSup_le (Set.forall_mem_image.mpr fun _ ↦ id)

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

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

Разделы

Аффилиация

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