res_apply — Mathlib

English

Restriction maps of the structure sheaf on an open set act by evaluating at the restricted point: the restriction is given by evaluating the section at i x.

Русский

Ограничение разделов структурной оболочки на открытом множестве действует по значению на ограниченной точке: ограничение задаётся вычислением раздела в точке i x.

LaTeX

$$$\\text{res\\_apply} (U,V,i,s,x) : ((structureSheaf R).1.map i.op\\, s).1 x = s.1 (i x)$$$

Lean4

@[simp]
theorem res_apply (U V : Opens (PrimeSpectrum.Top R)) (i : V ⟶ U) (s : (structureSheaf R).1.obj (op U)) (x : V) :
    ((structureSheaf R).1.map i.op s).1 x = (s.1 (i x) :) :=
  rfl

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