germ_residue — Mathlib

English

For U open in X and x ∈ U, the germ map interacts with the residue map to yield the evaluation map.

Русский

Для открытого подмножества U в X и x ∈ U, germs и резидуум взаимодействуют, давая карту оценки.

LaTeX

$$$$ \text{germ}_{U}(x) \circ \mathrm{residue}_{x} = \mathrm{evaluation}_{U}(x). $$$$

Lean4

@[reassoc]
theorem germ_residue (x hx) : X.presheaf.germ U x hx ≫ X.residue x = X.evaluation U x hx :=
  rfl

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