zeroLocus_def — Mathlib

English

The zero locus of a set of sections s over an open U is the intersection of the complements of the basic opens of each f ∈ s.

Русский

Нулевая область набора секций s над открытым U является пересечением дополнений базовых открытых для каждой f ∈ s.

LaTeX

$$$X.zeroLocus s = \\bigcap_{f \\in s} (X.basicOpen f)^{c}$$$

Lean4

theorem zeroLocus_def {U : X.Opens} (s : Set Γ(X, U)) : X.zeroLocus s = ⋂ f ∈ s, (X.basicOpen f).carrierᶜ :=
  rfl

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