cons_eq_append — Mathlib

English

Fin.cons x xs equals append (Fin.cons x Fin.elim0) xs composed with Fin.cast (Nat.add_comm ..).

Русский

Fin.cons x xs эквивалентно append (Fin.cons x Fin.elim0) xs, композиция с Fin.cast (Nat.add_comm ..).

LaTeX

$$$\\mathrm{cons}(x, xs) = \\mathrm{append}(\\mathrm{Fin.cons}(x,\\mathrm{Fin.elim0}), xs) \\circ \\mathrm{Fin.cast}(\\mathrm{Nat.add\\_comm}()).$$$

Lean4

/-- `Fin.cons` is the same as appending a one-tuple to the left. -/
theorem cons_eq_append (x : α) (xs : Fin n → α) :
    cons x xs = append (cons x Fin.elim0) xs ∘ Fin.cast (Nat.add_comm ..) := by funext i; simp [append_left_eq_cons]

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