mk_comp — Mathlib

English

The composition of two 2-cells in CatEnrichedOrdinary corresponds to chaining their Hom.mk representations: Hom.mk (α ≫ β) = Hom.mk α ≫ Hom.mk β.

Русский

Составление двух 2-ячейок в CatEnrichedOrdinary соответствует последовательной замене их через Hom.mk: Hom.mk (α ≫ β) = Hom.mk α ≫ Hom.mk β.

LaTeX

$$$ \\mathrm{Hom.mk}(\\alpha \\gg \\beta) = \\mathrm{Hom.mk}(\\alpha) \\;\\gg\\; \\mathrm{Hom.mk}(\\beta) $$$

Lean4

theorem mk_comp {X Y : CatEnrichedOrdinary C} {f g h : X ⟶ Y} (α : homEquiv f ⟶ homEquiv g)
    (β : homEquiv g ⟶ homEquiv h) : Hom.mk (α ≫ β) = Hom.mk α ≫ Hom.mk β :=
  rfl

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