ext — Mathlib

English

OverArrows is an extensional type: if two elements have equal val components, they are equal as OverArrows.

Русский

OverArrows является экстенсиональным типом: если два элемента имеют равные компоненты val, то они равны как OverArrows.

LaTeX

$$$\\forall F \\; \\eta \\; X \\; s \\; u \\; v,\\; u.val = v.val \\Rightarrow u = v$$$

Lean4

@[ext]
theorem ext {F : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {X : C} {s : yoneda.obj X ⟶ A} {u v : OverArrows η s} :
    u.val = v.val → u = v :=
  Subtype.ext

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