ext — Mathlib

English

Two morphisms f,g: a → b in Truncated n are equal if their underlying order homomorphisms are equal.

Русский

Два морфизма f,g: a → b в Truncated n равны, если их соответствующие упорядоченные гомоморфизмы совпадают.

LaTeX

$$$${n} {a b : \\mathrm{Truncated}(n)} (f,g : a \\to b), f^{\\mathrm{toOrderHom}} = g^{\\mathrm{toOrderHom}} \\Rightarrow f = g $$$$

Lean4

@[ext]
theorem ext {n} {a b : Truncated n} (f g : a ⟶ b) : f.toOrderHom = g.toOrderHom → f = g :=
  SimplexCategory.Hom.ext _ _

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