English
Let ι be a type with a unique element and M a topological R-module. The canonical linear isomorphism between the function space (ι → M) and M is given by evaluation at the unique element. Consequently, for every function f: ι → M, the image under the canonical map equals f(default).
Русский
Пусть ι — тип с единственным элементом, и M — топологический модуль над R. Каноническое линейное биективное соответствие между пространством функций (ι → M) и M определяется значения на единственном элементе. Следовательно, для каждой функции f: ι → M выполняется (funUnique ι R M)(f) = f(default).
LaTeX
$$$ (\mathrm{funUnique}_{ι,R,M})(f) = f(\mathrm{default}) \quad \text{для всех } f : ι \to M $$$
Lean4
@[simp]
theorem coe_funUnique : ⇑(funUnique ι R M) = Function.eval default :=
rfl
