sublistsLen_length — Mathlib

English

The length of the list of sublists of length n equals the binomial coefficient choose(|l|, n).

Русский

Длина списка подсписков длины n равна биномиальному коэффициенту C(|l|, n).

LaTeX

$$$\\operatorname{length}(\\operatorname{sublistsLen}(n, l)) = \\binom{\\operatorname{length}(l)}{n}$$$

Lean4

@[simp]
theorem sublistsLen_length : ∀ l : List α, sublistsLen l.length l = [l]
  | [] => rfl
  | a :: l => by
    simp only [length, sublistsLen_succ_cons, sublistsLen_length, map, sublistsLen_of_length_lt (lt_succ_self _),
      nil_append]

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