length_sublists'

Mathlib.Data.List.Sublists

URI: https://scilib.ai/kg/mathlib#List.length_sublists'

← MathLib Explorer

English

The number of sublists of a list of length n is 2^n.

Русский

Количество подсписков списка длины n равно 2^n.

LaTeX

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

Lean4

@[simp]
theorem length_sublists' : ∀ l : List α, length (sublists' l) = 2 ^ length l
  | [] => rfl
  | a :: l => by simp +arith only [sublists'_cons, length_append, length_sublists' l, length_map, length, Nat.pow_succ']

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru