zeroLocus_iInf — Mathlib

English

For a finite set of indices, the zero locus of the infimum over all I_i is the union over i of the zero loci of I_i.

Русский

Для конечного множества индексов нулевая локация инфимума над I_i равна объединению нулевых локаций I_i по всем i.

LaTeX

$$X.zeroLocus(U := U) ↑(⨅ i, I i) = ⋃ i, X.zeroLocus(U := U) (I i)$$

Lean4

theorem zeroLocus_iInf {X : Scheme.{u}} {U : X.Opens} {ι : Type*} (I : ι → Ideal Γ(X, U)) [Finite ι] :
    X.zeroLocus (U := U) ↑(⨅ i, I i) = (⋃ i, X.zeroLocus (U := U) (I i)) ∪ (↑U)ᶜ := by
  simpa using zeroLocus_biInf I Set.finite_univ

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