ext — Mathlib

English

Let X, Y be MagmaCat and f, g: X → Y. If f and g agree on every element x ∈ X, then f = g.

Русский

Пусть X, Y — объекты MagmaCat и f, g: X ⟶ Y. Если для каждого элемента x ∈ X выполняется f x = g x, то f = g.

LaTeX

$$$\\forall X,Y:\\mathrm{MagmaCat},\\forall f,g:\\,X \\to Y,\\left(\\forall x: X, f x = g x\\right) \\Rightarrow f = g$$$

Lean4

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

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