basicOpen_eq_bot_iff — Mathlib

English

For a reduced scheme X and a section s, X.basicOpen s equals the bottom if and only if s equals zero.

Русский

Для редуцированной схемы X выполняется: X.basicOpen s = ⊥ тогда и только тогда, когда s = 0.

LaTeX

$$$[IsReduced X] \Rightarrow (X.basicOpen(s) = \bot \leftrightarrow s = 0)$$$

Lean4

@[simp]
theorem basicOpen_eq_bot_iff {X : Scheme} [IsReduced X] {U : X.Opens} (s : Γ(X, U)) : X.basicOpen s = ⊥ ↔ s = 0 :=
  by
  refine ⟨eq_zero_of_basicOpen_eq_bot s, ?_⟩
  rintro rfl
  simp

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