ext' — Mathlib

English

Morphisms are determined by their underlying order maps; equality of order maps implies equality of morphisms.

Русский

Морфизмы определяются их базовыми отображениями; равенство отображений в порядке подразумевает равенство морфизмов.

LaTeX

$$$f.toOrderHom = g.toOrderHom \\Rightarrow f = g$$$

Lean4

theorem ext' {a b : SimplexCategory} (f g : SimplexCategory.Hom a b) : f.toOrderHom = g.toOrderHom → f = g :=
  id

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