zeroLocus_isClosed — Mathlib

English

For any open U and any set s of sections on U, the zero locus X.zeroLocus(s) is a closed subset of the underlying topological space of X.

Русский

Для любого открытого U и множества секций s над U нулевая локация X.zeroLocus(s) является замкнутым подмножеством подложного топологического пространства X.

LaTeX

$$IsClosed\left(X.zeroLocus(s)\right)$$

Lean4

theorem zeroLocus_isClosed {U : Opens X} (s : Set (X.presheaf.obj (op U))) : IsClosed (X.zeroLocus s) :=
  by
  apply isClosed_biInter
  intro i _
  simp only [isClosed_compl_iff]
  exact Opens.isOpen (X.basicOpen i)

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