hom_ext — Mathlib

English

Uniqueness of morphisms in OneTruncation₂ determined by their edges holds, supporting a strong extensionality principle.

Русский

Уникальность морфизмов в OneTruncation₂ определяется по их рёбрам, поддерживая сильную экстензонность.

LaTeX

$$$$\text{OneTruncation₂.hom_ext}$$$$

Lean4

@[ext]
theorem hom_ext {S : SSet.Truncated 2} {x y : OneTruncation₂ S} {f g : x ⟶ y} : f.edge = g.edge → f = g :=
  OneTruncation₂.Hom.ext

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