hom_injective — Mathlib

English

The map Hom(X,Y) → ToHom X Y is injective; i.e., distinct morphisms have distinct underlying functions.

Русский

Отображение морфизмов Hom(X,Y) → ToHom X Y инъективно; различные морфизмы дают различные базовые функции.

LaTeX

$$$\text{inj}((\,\cdot\,)) : \forall f,g:\,X \to Y, ((f) = (g)) \Rightarrow (f = g)$$$

Lean4

theorem hom_injective {X Y : C} : Function.Injective (hom : (X ⟶ Y) → ToHom X Y) :=
  hom_bijective.injective

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