mem_zeroLocus_iff — Mathlib

English

A point x belongs to Z(s) if and only if for every f in s, x does not belong to D(f).

Русский

Точка x принадлежит Z(s) тогда и только тогда, когда для любого f из s, x не принадлежит D(f).

LaTeX

$$x \in X.zeroLocus(s) \iff \forall f \in s, x \notin X.basicOpen(f)$$

Lean4

@[simp]
theorem mem_zeroLocus_iff {U : Opens X} (s : Set (X.presheaf.obj (op U))) (x : X) :
    x ∈ X.zeroLocus s ↔ ∀ f ∈ s, x ∉ X.basicOpen f := by simp [zeroLocus]

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