comp_comp — Mathlib

English

The action of a composed morphism corresponds to composing the actions of its factors on pseudoelements.

Русский

Действие композиции морфизмов на псевдоэлементах равно композиции действий их факторов.

LaTeX

$$$\\mathrm{pseudoApply}(g\\circ f) = \\mathrm{pseudoApply}(g) \\circ \\mathrm{pseudoApply}(f)$$$

Lean4

/-- Composition of functions on pseudoelements is composition of morphisms. -/
theorem comp_comp {P Q R : C} (f : P ⟶ Q) (g : Q ⟶ R) : g ∘ f = f ≫ g :=
  funext fun _ => (comp_apply _ _ _).symm

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