zeroLocus_singleton — Mathlib

English

The zero locus of a singleton {f} equals the complement of the basic open set defined by f, i.e. X.zeroLocus({f}) = (D(f))^c.

Русский

Нулевая локация одиночного элемента {f} равна дополнению к базовой открытой D(f); то есть Z({f}) = D(f)^c.

LaTeX

$$X.zeroLocus\left\{f\right\} = \left(X.basicOpen(f)\right)^{c}$$

Lean4

theorem zeroLocus_singleton {U : Opens X} (f : X.presheaf.obj (op U)) : X.zeroLocus { f } = (X.basicOpen f).carrierᶜ :=
  by simp [zeroLocus]

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