ext — Mathlib

English

Extensionality: two lattice homomorphisms are equal if they are equal on all inputs.

Русский

Расширение по значениям: два гомоморфизма равны, если на каждом аргументе они совпадают.

LaTeX

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

Lean4

@[ext]
theorem ext {f g : LatticeHom α β} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

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