instFunLike — Mathlib

English

The space of continuous affine maps is equipped with a FunLike structure, making evaluation function and composition behave like functions.

Русский

Обозначение пространства непрерывных аффинных отображений обладает структурой FunLike, обеспечивающей поведение операции применения и композиции как функций.

LaTeX

$$instance : FunLike (P \toᴬ[R] Q) P Q$$

Lean4

instance : FunLike (P →ᴬ[R] Q) P Q where
  coe f := f.toAffineMap
  coe_injective' _ _ h := toAffineMap_injective <| DFunLike.coe_injective h

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