evaluation_ne_zero_iff_mem_basicOpen

English

Let X be a Locally Ringed Space, U an open, x ∈ U, and f ∈ X.presheaf.obj (op U). Then the evaluation at x is nonzero if and only if x lies in the basic open where f is nonvanishing.

Русский

Пусть X — локально кольцевое пространство, U — открыто, x ∈ U и f ∈ X.presheaf.obj (op U). Тогда evaluation x f не равно нулю тогда и только тогда, когда x ∈ basicOpen(f).

LaTeX

$$$ X.\\mathrm{evaluation}\\, x\\, f \\neq 0 \\iff x \\in X.\\mathrm{toRingedSpace}.basicOpen\\, f $$$

Lean4

theorem evaluation_ne_zero_iff_mem_basicOpen (x : U) (f : X.presheaf.obj (op U)) :
    X.evaluation x f ≠ 0 ↔ x.val ∈ X.toRingedSpace.basicOpen f := by simp

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