assocLeft — Mathlib

English

Left associator for HolorIndex: HolorIndex (ds₁ ++ (ds₂ ++ ds₃)) → HolorIndex (ds₁ ++ ds₂ ++ ds₃).

Русский

Левая ассоциативность для HolorIndex: обратная к правой ассоциации.

LaTeX

$$assocLeft : HolorIndex (ds₁ ++ (ds₂ ++ ds₃)) → HolorIndex (ds₁ ++ ds₂ ++ ds₃)$$

Lean4

/-- Left associator for `HolorIndex` -/
def assocLeft : HolorIndex (ds₁ ++ (ds₂ ++ ds₃)) → HolorIndex (ds₁ ++ ds₂ ++ ds₃) :=
  cast (congr_arg HolorIndex (append_assoc ds₁ ds₂ ds₃).symm)

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