ideal_mono

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

If I ≤ J for ideal data, then I.ideal ≤ J.ideal.

Русский

Если I ≤ J для данных идеалов, то I.ideal ≤ J.ideal.

LaTeX

$$$ I \le J \Rightarrow I.ideal \le J.ideal $$$

Lean4

theorem ideal_mono : Monotone (ideal (X := X)) :=
  strictMono_ideal.monotone

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

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

Разделы

Аффилиация

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