instFunLike — Mathlib

English

There is a FunLike instance for BoundedLatticeHom, identifying the function with the underlying coe.

Русский

Существует экземпляр FunLike для BoundedLatticeHom, отождествляющий функцию с основанной конверсией.

LaTeX

$$$\\text{instFunLike}:\\mathrm{FunLike}(\\mathrm{BoundedLatticeHom}(\\alpha,\\beta),\\alpha,\\beta)$$$

Lean4

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

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