hom_ext — Mathlib

English

In the comma category for L: A → T and R: B → T, two morphisms X ⟶ Y are equal whenever their left and right components are equal.

Русский

В комма-категории по L: A → T и R: B → T два морфизма X ⟶ Y равны тогда и только тогда, когда их левые и правые компоненты совпадают.

LaTeX

$$$f,g: X \to Y$ в Comma(L,R) с $f.left = g.left$ и $f.right = g.right$ удовлетворяют $f = g$.$$

Lean4

@[ext]
theorem hom_ext (f g : X ⟶ Y) (h₁ : f.left = g.left) (h₂ : f.right = g.right) : f = g :=
  CommaMorphism.ext h₁ h₂

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