ofIdeals_mono

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

The map I ↦ ofIdeals(I) is monotone: I ≤ J implies ofIdeals(I) ≤ ofIdeals(J).

Русский

Карта I ↦ ofIdeals(I) монотонна: I ≤ J ⇒ ofIdeals(I) ≤ ofIdeals(J).

LaTeX

$$$ I \le J \Rightarrow \operatorname{ofIdeals}(I) \le \operatorname{ofIdeals}(J) $$$

Lean4

theorem ofIdeals_mono : Monotone (ofIdeals (X := X)) :=
  IdealSheafData.gci.gc.monotone_u

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

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

Разделы

Аффилиация

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