instFunLike — Mathlib

English

BoundedOrderHom α β has a natural function-like structure: the carrier is the underlying toFun, and two elements are equal if their underlying functions are equal.

Русский

У BoundedOrderHom α β имеется естественная структура как у отображений: носитель — это toFun, и два элемента равны, если их базовые функции равны.

LaTeX

$$$\\text{BoundedOrderHom }(\\alpha,\\beta)\\;\\text{is a FunLike type with } f\\mapsto f.toFun,\\; (f=g)\\iff (f.toFun=g.toFun).$$$

Lean4

instance : FunLike (BoundedOrderHom α β) α β where
  coe f := f.toFun
  coe_injective' f g h := by obtain ⟨⟨_, _⟩, _⟩ := f; obtain ⟨⟨_, _⟩, _⟩ := g; congr

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