apply — Mathlib

English

There is a natural projection from ContDiffMapSupportedIn E F n K to the space of functions E → F, given by f ↦ f.

Русский

Существует естественная проекция из ContDiffMapSupportedIn E F n K в пространство функций E → F, отображающая f на саму функцию f.

LaTeX

$$$ (\mathrm{ContDiffMapSupportedIn.Simps.apply})(f) = f $$$

Lean4

/-- See note [custom simps projection]. -/
def apply (f : 𝓓^{n}_{K}(E, F)) : E → F :=
  f

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