vanishingIdeal_union — Mathlib

English

For two subsets t and t' of the PrimeSpectrum(R), the vanishing ideal of their union is the infimum (intersection) of their vanishing ideals:

Русский

Для двух подмножеств t и t' простого спектра R ванishing ideals совокупности равны взаимному пересечению:

LaTeX

$$$\\mathrm{vanishingIdeal}(t \\cup t') = \\mathrm{vanishingIdeal}(t) \\sqcap \\mathrm{vanishingIdeal}(t').$$$

Lean4

theorem vanishingIdeal_union (t t' : Set (PrimeSpectrum R)) :
    vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t' :=
  (gc R).u_inf

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