eval_germ — Mathlib

English

Evaluating the germ of a smooth function at a point x recovers the function value at x.

Русский

Оценка жёрма гладкой функции в точке x восстанавливает значение функции в x.

LaTeX

$$$$ \\text{eval}_{x}((\\text{presheaf}.\\text{germ } U x f)) = f(x). $$$$

Lean4

@[simp]
theorem eval_germ (U : Opens M) (x : M) (hx : x ∈ U) (f : (smoothSheafCommRing IM I M R).presheaf.obj (op U)) :
    smoothSheafCommRing.eval IM I M R x ((smoothSheafCommRing IM I M R).presheaf.germ U x hx f) = f ⟨x, hx⟩ :=
  smoothSheafCommRing.evalHom_germ IM I M R U x hx f

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