append_assoc — Mathlib

English

ListBlank.append is associative with List construction: append (l1 ++ l2) l3 = append l1 (append l2 l3).

Русский

Операция Append для ListBlank ассоциативна: append (l1 ++ l2) l3 = append l1 (append l2 l3).

LaTeX

$$$\forall {\Gamma} [Inhabited(\Gamma)] (l_1 l_2 : List(\Gamma)) (l_3 : ListBlank(\Gamma)),\ ListBlank.append (l_1 ++ l_2) l_3 = ListBlank.append l_1 (ListBlank.append l_2 l_3)$$$

Lean4

theorem append_assoc {Γ} [Inhabited Γ] (l₁ l₂ : List Γ) (l₃ : ListBlank Γ) :
    ListBlank.append (l₁ ++ l₂) l₃ = ListBlank.append l₁ (ListBlank.append l₂ l₃) :=
  by
  refine l₃.induction_on fun l ↦ ?_
  simp only [ListBlank.append_mk, List.append_assoc]

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