Γevaluation_eq_zero_iff_notMem_basicOpen

English

Replacing the evaluation with the Γ-evaluation yields the same vanishing criterion: the Γ-evaluation at x of f is zero exactly when x is not in the basic open of f.

Русский

Замещая оценку Γ-оценкой, получаем аналогичный критерий: Γ-оценка в x от f равна нулю тогда, когда x не принадлежит базовому открытому множеству f.

LaTeX

$$$ X.\\Gamma\\mathrm{evaluation}\\, x\\, f = 0 \\iff x \\notin X.\\mathrm{toRingedSpace}.basicOpen\\, f $$$

Lean4

@[simp]
theorem Γevaluation_eq_zero_iff_notMem_basicOpen (x : X) (f : X.presheaf.obj (op ⊤)) :
    X.Γevaluation x f = 0 ↔ x ∉ X.toRingedSpace.basicOpen f :=
  evaluation_eq_zero_iff_notMem_basicOpen X ⟨x, show x ∈ ⊤ by trivial⟩ f

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