simplicialInsert_length — Mathlib

English

Applying simplicialInsert increases the length of a list by exactly 1.

Русский

Применение simplicialInsert увеличивает длину списка ровно на 1.

LaTeX

$$$\\\\text{length}(simplicialInsert(a,L)) = \\text{length}(L) + 1$.$$

Lean4

/-- `simplicialInsert` just adds one to the length. -/
theorem simplicialInsert_length (a : ℕ) (L : List ℕ) : (simplicialInsert a L).length = L.length + 1 := by
  induction L generalizing a with
  | nil => rfl
  | cons head tail h_rec =>
    dsimp only [simplicialInsert, List.length_cons]
    split_ifs with h <;> simp only [List.length_cons, h_rec (a + 1)]

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