ext — Mathlib

English

Extensionality principle for CommMonCat morphisms: two morphisms are equal if they agree on all carriers.

Русский

Принцип экстенсивности для морфизмов CommMonCat: два морфизма равны, если они совпадают на всех носителях.

LaTeX

$$$\forall X,Y:\ CommMonCat,\ f,g:\, X \to Y,\ (\forall x:\, X.carrier, f(x)=g(x)) \Rightarrow f=g$$$

Lean4

@[to_additive (attr := ext)]
theorem ext {X Y : CommMonCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
  ConcreteCategory.hom_ext _ _ w

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