mk₅ — Mathlib

English

Equality: mk5 f g h i j = (mk4 g h i j).precomp f.

Русский

Равенство: mk5 f g h i j = (mk4 g h i j).precomp f.

LaTeX

$$$ \text{mk}_5 f\,g\,h\,i\,j = (\text{mk}_4\, g\, h\, i\, j).\text{precomp } f $$$

Lean4

/-- Constructor for `ComposableArrows C 5`. -/
@[simp]
def mk₅ {X₀ X₁ X₂ X₃ X₄ X₅ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) (j : X₄ ⟶ X₅) :
    ComposableArrows C 5 :=
  (mk₄ g h i j).precomp f

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