English
For the sheaf of smooth maps from M to N, on an open set U, the value is exactly the type of $(IM, (unop U))$-smooth maps from U to N.
Русский
Для непрерывной (гладкой) оболочки от M в 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
/-- The sheaf of smooth functions from `M` to `N`, as a sheaf of types. -/
def smoothSheaf : TopCat.Sheaf (Type u) (TopCat.of M) :=
(contDiffWithinAt_localInvariantProp (I := IM) (I' := I) ∞).sheaf M N