comp_def — Mathlib

English

For f: X → Y and g: Y → Z in the wide subcategory P, the underlying morphism of the composite f ≫ g is the composition of the underlying morphisms f.1 and g.1 in C.

Русский

Для f: X → Y и g: Y → Z в широкой подпредкатегории P подмножество соответствующей композиции f ≫ g выполняется тождество: (f ≫ g).1 = (f.1 ≫ g.1).

LaTeX

$$$ (f \gg g).1 = (f.1 \gg g.1) $$$

Lean4

@[simp]
theorem comp_def {X Y Z : WideSubcategory P} (f : X ⟶ Y) (g : Y ⟶ Z) : (f ≫ g).1 = (f.1 ≫ g.1 : X.obj ⟶ Z.obj) :=
  rfl

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