support_eq_top_iff — Mathlib

English

Over a reduced X, the only ideal with full support is the bottom ideal; i.e., Supp(I) = ⊤ iff I = ⊥.

Русский

Для приведённой X единственный идеал с полной поддержкой — это нижний.

LaTeX

$$[IsReduced X] ⇒ (I.\\mathrm{support} = \\top \\iff I = \\bot)$$

Lean4

theorem support_eq_top_iff [IsReduced X] {I : X.IdealSheafData} : I.support = ⊤ ↔ I = ⊥ := by
  rw [← top_le_iff, le_support_iff_le_vanishingIdeal, vanishingIdeal_top, nilradical_eq_bot, le_bot_iff]

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