length_sublistsLen — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem length_sublistsLen : ∀ (n) (l : List α), length (sublistsLen n l) = Nat.choose (length l) n
  | 0, l => by simp
  | _ + 1, [] => by simp
  | n + 1, a :: l => by
    rw [sublistsLen_succ_cons, length_append, length_sublistsLen (n + 1) l, length_map, length_sublistsLen n l,
      length_cons, Nat.choose_succ_succ, Nat.add_comm]

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