codisjoint_zeroLocus — Mathlib

English

The zero locus is codisjoint to the open set U, reflecting that points in the zero locus are not contained in U in a mutual sense.

Русский

Нулевая область кодисjoint по отношению к открытому множеству U, что отражает отсутствие общих точек между нулевой областью и U в взаимном смысле.

LaTeX

$$$Codisjoint\\bigl(X.zeroLocus s, U\\bigr)$$$

Lean4

theorem codisjoint_zeroLocus {U : X.Opens} (s : Set Γ(X, U)) : Codisjoint (X.zeroLocus s) U :=
  by
  have (x : X) : ∀ f ∈ s, x ∈ X.basicOpen f → x ∈ U := fun _ _ h ↦ X.basicOpen_le _ h
  simpa [codisjoint_iff_le_sup, Set.ext_iff, or_iff_not_imp_left]

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