hom_ext — Mathlib

English

In UniformSpaceCat, equality of morphisms is determined by their carrier functions; i.e., if two morphisms have the same underlying function, they are equal.

Русский

В категории равномерных пространств равенство морфизмов определяется их базовыми функциями; если две гомоморфизмы имеют одну и ту же отображающую функцию, они равны.

LaTeX

$$$\forall X,Y:\ UniformSpaceCat,\forall f,g:\,X\to Y,\ (f:X\to Y)=(g:X\to Y)\Rightarrow f=g$$$

Lean4

@[ext]
theorem hom_ext {X Y : UniformSpaceCat} {f g : X ⟶ Y} (h : (f : X → Y) = g) : f = g :=
  Hom.ext (Subtype.ext h)

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