base_comp — Mathlib

English

Variant of comp_eq expressing the same equality in a different presentation of the instCategoryStructHom comp.

Русский

Вариант comp_eq, выражающий ту же самую эквивалентность в другой форме представления comp для instCategoryStructHom.

LaTeX

$$$ (\\alpha \\gg \\beta) = Hom.mk (Hom.base \\alpha \\gg Hom.base \\beta) $$$

Lean4

@[simp]
theorem base_comp {X Y : CatEnrichedOrdinary C} {f g h : X ⟶ Y} (α : f ⟶ g) (β : g ⟶ h) :
    Hom.base (α ≫ β) = Hom.base α ≫ Hom.base β :=
  rfl

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