hom_ext — Mathlib

English

Morphisms are determined by their effect on arguments: if f,g: X ⟶ Y satisfy f(x) = g(x) for all x, then f = g.

Русский

Гомоморфизмы детерминированы по значению на каждом элементе: если f(x) = g(x) для всех x, то f = g.

LaTeX

$$$\\forall X,Y: FintypeCat,\\; \\forall f,g: X \\to Y,\\; (\\forall x: X,\\; f(x) = g(x)) \\Rightarrow f = g$$$

Lean4

@[ext]
theorem hom_ext {X Y : FintypeCat} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g :=
  by
  funext
  apply h

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