funLike — Mathlib

English

The structure AlgHom R A B carries a FunLike instance, i.e., its elements act as functions A → B with equality determined by their action on inputs.

Русский

Структура AlgHom R A B обладает инстансом FunLike: элементы действуют как функции A → B, и равенство определяется их действием на аргументах.

LaTeX

$$$\\text{AlgHom } R A B\\;\\text{ is a FunLike object with } f: A \\to B$.$$

Lean4

instance funLike : FunLike (A →ₐ[R] B) A B where
  coe f := f.toFun
  coe_injective' f g
    h := by
    rcases f with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
    rcases g with ⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩
    congr

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