update_cons_zero — Mathlib

English

Updating the first position after enclosing with cons is the same as enclosing with the new head: update (cons x p) 0 z = cons z p.

Русский

Обновление на нулевой позиции после конструирования cons эквивалентно конструированию cons с новым значением: update (cons x p) 0 z = cons z p.

LaTeX

$$$\\mathrm{update}(\\\\mathrm{cons}(x,p),0,z) = \\\\mathrm{cons}(z,p)$$$

Lean4

/-- Adding an element at the beginning of a tuple and then updating it amounts to adding it
directly. -/
@[simp]
theorem update_cons_zero : update (cons x p) 0 z = cons z p :=
  by
  ext j
  cases j using Fin.cases <;> simp

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