vanishingIdeal_sSup — Mathlib

English

For a set Z of closed subsets, the vanishing ideal of their supremum equals the infimum over Z of the vanishing ideals.

Русский

Для множества Z замкнутых подмножеств идеал исчезновения их супремума равен Infimum по Z от соответствующих идеалов исчезновения.

LaTeX

$$\\operatorname{vanishingIdeal}(\\mathrm{sSup}\\,Z) = \\bigwedge_{z\\in Z} \\operatorname{vanishingIdeal}(z)$$

Lean4

@[simp]
theorem vanishingIdeal_sSup (Z : Set (Closeds X)) : vanishingIdeal (sSup Z) = ⨅ z ∈ Z, vanishingIdeal z :=
  gc.u_sInf

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