Γevaluation_ne_zero_iff_mem_basicOpen

English

The Γ-evaluation is nonzero at x if and only if x lies in the basic open where f does not vanish.

Русский

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

LaTeX

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

Lean4

theorem Γevaluation_ne_zero_iff_mem_basicOpen (x : X) (f : X.presheaf.obj (op ⊤)) :
    X.Γevaluation x f ≠ 0 ↔ x ∈ X.toRingedSpace.basicOpen f :=
  evaluation_ne_zero_iff_mem_basicOpen X ⟨x, show x ∈ ⊤ by trivial⟩ f

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