instFunLike — Mathlib

English

SpectralMap α β carries a FunLike structure, with the function part given by toFun.

Русский

SpectralMap α β имеет структуру FunLike, причём отображение задаётся через toFun.

LaTeX

$$$\text{SpectralMap}(\alpha,\beta)\text{ оснащён структурой FunLike } f\mapsto f.toFun. $$$

Lean4

instance instFunLike : FunLike (SpectralMap α β) α β
    where
  coe := SpectralMap.toFun
  coe_injective' f g h := by cases f; cases g; congr

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