orderedInsert_length — Mathlib

English

For any list L and any element a, the length of L.orderedInsert(r,a) is length(L) + 1.

Русский

Для любого списка L и элемента a, длина L.orderedInsert(r,a) равна длине L плюс 1.

LaTeX

$$$$ \forall L:\mathrm{List}(\alpha),\; \operatorname{length}(\mathrm{orderedInsert}(r,a,L)) = \operatorname{length}(L) + 1. $$$$

Lean4

theorem orderedInsert_length : ∀ (L : List α) (a : α), (L.orderedInsert r a).length = L.length + 1
  | [], _ => rfl
  | hd :: tl, a => by
    dsimp [orderedInsert]
    split_ifs <;> simp [orderedInsert_length tl]

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