hom_ext — Mathlib

English

Two morphisms in the thickened simplicial category are equal if all their components agree after evaluating at every index.

Русский

Два морфизма в утолщённой симпликальной категории равны, если их компоненты совпадают на всех индексах.

LaTeX

$$$$ \text{HomExt} \; (f,g) : (\forall n, f.app(n)=g.app(n)) \Rightarrow f=g $$$$

Lean4

@[ext]
theorem hom_ext {J : Type*} [LinearOrder J] (i j : SimplicialThickening J) (x y : i ⟶ j) (h : ∀ t, t ∈ x.I ↔ t ∈ y.I) :
    x = y := by
  apply Path.ext
  ext
  apply h

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