hom_ext — Mathlib

English

Two morphisms f,g: X → Y are equal whenever their underlying functions agree on every element of X; i.e., if f.hom = g.hom, then f = g.

Русский

Два морфизма f,g: X → Y равны тогда и только тогда, когда их действующие на элементы функции совпадают; то есть если f.hom = g.hom, то f = g.

LaTeX

$$$$ f = g \quad \text{whenever } f_{\text{hom}} = g_{\text{hom}}. $$$$

Lean4

@[ext]
theorem hom_ext {X Y : BoolAlg} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g :=
  Hom.ext hf

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