zeroLocus_univ — Mathlib

English

For any open U, the zero locus of Set.univ with respect to U is the complement of U: zeroLocus(Set.univ) = (↑U)ᶜ.

Русский

Для любого открытого множества U нулевая область Set.univ равна комплементу U: zeroLocus(Set.univ) = U^c.

LaTeX

$$$X.zeroLocus (U := U) Set.univ = (\uparrow U)^{c}$$$

Lean4

@[simp]
theorem zeroLocus_univ {U : X.Opens} : X.zeroLocus (U := U) Set.univ = (↑U)ᶜ :=
  by
  ext x
  simp only [Scheme.mem_zeroLocus_iff, Set.mem_univ, forall_const, Set.mem_compl_iff, SetLike.mem_coe, ← not_exists,
    not_iff_not]
  exact ⟨fun ⟨f, hf⟩ ↦ X.basicOpen_le f hf, fun _ ↦ ⟨1, by rwa [X.basicOpen_of_isUnit isUnit_one]⟩⟩

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