append_head — Mathlib

English

The head of an appended NeWord is the head of the first part: head(append w1 hne w2) = head(w1).

Русский

Голова объединённого слова равна голове первого слагаемого: head(append w1 hne w2) = head(w1).

LaTeX

$$$$\\text{head}(\\text{append}(w_1,\\, hne, w_2)) = w_1.head.$$$$

Lean4

@[simp]
theorem append_head {i j k l} {w₁ : NeWord M i j} {hne : j ≠ k} {w₂ : NeWord M k l} :
    (append w₁ hne w₂).head = w₁.head :=
  rfl

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