applyId_cons — Mathlib

English

When applying to a cons cell, the result checks the head first; if x equals the head's first component, return the head's second component; otherwise applyId to the tail.

Русский

При применении к конс-ячейке сначала проверяем голову: если x равен её первой компоненте, возвращаем вторую компоненту; иначе применяем applyId к хвосту.

LaTeX

$$$\text{List.applyId}((y,z) :: xs)\ x = \begin{cases} z & y = x \\ \text{List.applyId}\ xs\ x & \text{иначе}. \end{cases}$$$

Lean4

@[simp]
theorem applyId_cons [DecidableEq α] (xs : List (α × α)) (x y z : α) :
    List.applyId ((y, z) :: xs) x = if y = x then z else List.applyId xs x :=
  by
  simp only [List.applyId, List.dlookup, eq_rec_constant, Prod.toSigma, List.map]
  split_ifs <;> rfl

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