ext — Mathlib

English

Two Coheyting homomorphisms that agree on every input are equal.

Русский

Две когейтинговые гомоморфизмы совпадают на всех входах тогда и только тогда равны между собой.

LaTeX

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

Lean4

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

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