openToLocalization_apply — Mathlib

English

The coercion maps align: the coe of openToLocalization equals the evaluation at x.

Русский

Коэффициентная карта openToLocalization совпадает с вычислением в точке x.

LaTeX

$$$openToLocalization(R, U, x, hx) = \\lambda s . s(x).$$$

Lean4

theorem openToLocalization_apply (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpectrum.Top R) (hx : x ∈ U)
    (s : (structureSheaf R).1.obj (op U)) : openToLocalization R U x hx s = s.1 ⟨x, hx⟩ :=
  rfl

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