instFunLike — Mathlib

English

The collection of order-preserving maps α → β forms a FunLike structure with the toFun projection.

Русский

Множество отображений, сохраняющих порядок, образует структуру FunLike с проекцией toFun.

LaTeX

$$$\text{OrderHom }(\alpha,\beta) \text{ has a }\text{FunLike} \text{ structure via } toFun$$$

Lean4

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

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