instFunLike — Mathlib

English

The Schwartz space carries a canonical FunLike structure, i.e., evaluation by a function is well-defined.

Русский

Пространство Шварца несёт каноническую структуру FunLike, т.е. вычисление по функции корректно определено.

LaTeX

$$$ \text{SchwartzMap.instFunLike is well-defined} $$$

Lean4

instance instFunLike : FunLike 𝓢(E, F) E F where
  coe f := f.toFun
  coe_injective' f g h := by cases f; cases g; congr

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