instFunLike — Mathlib

English

There is a FunLike instance for OrderRingHom, i.e., each OrderRingHom α β behaves as a function α → β with a canonical function-like coercion and injectivity under equality of functions.

Русский

Существует экземпляр FunLike для OrderRingHom, то есть каждый OrderRingHom α β ведёт себя как функция α → β с каноническим приводом и инъективностью по равенству функций.

LaTeX

$$$\\text{OrderRingHom.instFunLike}: \\text{FunLike }(α \\to+*o β) α β$$$

Lean4

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

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