length_sublists — Mathlib

English

Let l be a finite list. The number of sublists of l equals 2^{length(l)}.

Русский

Пусть l — конечный список. Число подсписков списка l равно 2^{длина(l)}.

LaTeX

$$$\\operatorname{length}(\\operatorname{sublists}(l)) = 2^{\\operatorname{length}(l)}$$$

Lean4

@[simp]
theorem length_sublists (l : List α) : length (sublists l) = 2 ^ length l := by
  simp only [sublists_eq_sublists', length_map, length_sublists', length_reverse]

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