homMk₅ — Mathlib

English

In the 5-step construction homMk5, the second component (index 1) equals the given morphism app1.

Русский

В части конструирования homMk5 пятый размер-для узла 1 совпадает с данным морфизмом app1.

LaTeX

$$$((homMk_5\; app_0\; app_1\; app_2\; app_3\; app_4\; app_5\; w_0\; w_1\; w_2\; w_3\; w_4).app 1) = app_1$$$

Lean4

/-- Constructor for morphisms in `ComposableArrows C 5`. -/
def homMk₅ : f ⟶ g :=
  homMkSucc app₀ (homMk₄ app₁ app₂ app₃ app₄ app₅ w₁ w₂ w₃ w₄) w₀

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