vanishingIdeal_union — Mathlib

English

The vanishing ideal of a union of two subsets equals the infimum (meet) of the vanishing ideals of the subsets.

Русский

Общий идеал vanishing для объединения двух множеств равен их инфимууму (inf) в структуре идеалов.

LaTeX

$$$ \operatorname{vanishingIdeal}(t \cup t') = \operatorname{vanishingIdeal}(t) \wedge \operatorname{vanishingIdeal}(t') $$$

Lean4

theorem vanishingIdeal_union (t t' : Set (ProjectiveSpectrum 𝒜)) :
    vanishingIdeal (t ∪ t') = vanishingIdeal t ⊓ vanishingIdeal t' := by ext1; exact (gc_ideal 𝒜).u_inf

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