instFunLike — Mathlib

English

Two lattice homomorphisms are equal if they agree on every input element.

Русский

Два гомоморфизма решетки равны, если они совпадают на каждом элементе.

LaTeX

$$$\forall f,g:\mathrm{LatticeHom}(\alpha,\beta),\ (\forall a\in \alpha,\ f(a)=g(a)) \Rightarrow f=g.$$$

Lean4

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

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