hom_ext — Mathlib

English

Morphisms f,g : X ⟶ Y in SimplicialObject C are equal if all their components on every index n agree: for all n, f.app n = g.app n.

Русский

Морфизмы f,g : X ⟶ Y в SimplicialObject C равны, если для каждого индекса n выполнено f.app n = g.app n.

LaTeX

$$$$ \forall n, f.app n = g.app n \implies f = g $$$$

Lean4

@[ext]
theorem hom_ext {X Y : SimplicialObject C} (f g : X ⟶ Y) (h : ∀ (n : SimplexCategoryᵒᵖ), f.app n = g.app n) : f = g :=
  NatTrans.ext (by ext; apply h)

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