mem_zeroLocus_iff — Mathlib

English

Membership of a point x in the zero locus is equivalent to the point not lying in any basic open corresponding to a section in s.

Русский

Принадлежность точки x нулевой области эквивалентна тому, что точка не лежит в каком-либо базовом открытом, соответствующем секции из s.

LaTeX

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

Lean4

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

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