mk_list_eq_sum_pow — Mathlib

English

Let α be a type. The cardinality of all finite lists over α equals the sum over all lengths n of |α|^n.

Русский

Пусть α — тип. Кардинальность множества всех конечных списков над α равна сумме по всем длинам n равной |α|^n.

LaTeX

$$$|\\mathrm{List} \\;\\alpha| = \\sum_{n \\in \\mathbb{N}} |\\alpha|^{n}$$$

Lean4

theorem mk_list_eq_sum_pow (α : Type u) : #(List α) = sum fun n : ℕ => #α ^ n :=
  calc
    #(List α) = #(Σ n, List.Vector α n) := mk_congr (Equiv.sigmaFiberEquiv List.length).symm
    _ = sum fun n : ℕ => #α ^ n := by simp

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