vanishingIdeal_antimono

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

English

If S and T are closed subsets of X with S ≤ T, then vanishingIdeal(T) ≤ vanishingIdeal(S).

Русский

Если S ⊆ T — две замкнутые подсистемы X, тогда vanishingIdeal(T) ≤ vanishingIdeal(S).

LaTeX

$$If $S \\le T$, then $\\operatorname{vanishingIdeal}(T) \\leq \\operatorname{vanishingIdeal}(S).$$$

Lean4

theorem vanishingIdeal_antimono {S T : Closeds X} (h : S ≤ T) : vanishingIdeal T ≤ vanishingIdeal S :=
  gc.monotone_u h

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

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

Разделы

Аффилиация

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