length_sym2 — Mathlib

English

The length of xs.sym2 equals the binomial coefficient choose(length(xs) + 1, 2).

Русский

Длина xs.sym2 равна биномиальному коэффициенту выбрать(length(xs) + 1, 2).

LaTeX

$$$$ |xs.sym2| = \\binom{|xs| + 1}{2} $$$$

Lean4

theorem length_sym2 {xs : List α} : xs.sym2.length = Nat.choose (xs.length + 1) 2 := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    rw [List.sym2, length_append, length_map, length_cons, Nat.choose_succ_succ, ← ih, Nat.choose_one_right]

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