ext — Mathlib

English

In the category of elements for a functor F: C ⥤ Type, morphisms are determined by their underlying value; two morphisms are equal if their underlying values are equal.

Русский

В категории элементов для функторa F: C ⥤ Type морфизмы определяются их основанным значением; два морфизма равны, если их значения равны.

LaTeX

$$$\\text{Theorem }\\text{ext} \\ (F : C \\to Type_w)\\ {x y : F.Elements} (f g : x \\to y) (w : f.val = g.val) : f = g$$$

Lean4

@[ext]
theorem ext (F : C ⥤ Type w) {x y : F.Elements} (f g : x ⟶ y) (w : f.val = g.val) : f = g :=
  Subtype.ext w

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