coeFun — Mathlib

English

The definitional equality asserts that the object of smooth sheaf over U is exactly the space of $(IM,I)$-smooth maps from U to N.

Русский

Определённое равенство утверждает, что объект гладкой оболочки над U равен набору гладких отображений из U в N, сочетающим структуры IM и I.

LaTeX

$$$ (\text{smoothSheaf IM I M N}).presheaf.obj U = C^∞\langle IM,(unop U): Opens M; I,N \rangle $$$

Lean4

instance coeFun (U : (Opens (TopCat.of M))ᵒᵖ) :
    CoeFun ((smoothSheaf IM I M N).presheaf.obj U) (fun _ ↦ ↑(unop U) → N) :=
  (contDiffWithinAt_localInvariantProp ∞).sheafHasCoeToFun _ _ _

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