mk_list_eq_mk — Mathlib

English

For an infinite α, the cardinality of the type of finite lists over α equals the cardinality of α: #List(α) = #α.

Русский

Для бесконечного множества α кардинальность множества всех конечных списков над α равна кардинальности α: #(List α) = #α.

LaTeX

$$$|\\mathrm{List}(\\alpha)| = |\\alpha|$$$

Lean4

@[simp]
theorem mk_list_eq_mk (α : Type u) [Infinite α] : #(List α) = #α :=
  have H1 : ℵ₀ ≤ #α := aleph0_le_mk α
  Eq.symm <|
    le_antisymm ((le_def _ _).2 ⟨⟨fun a => [a], fun _ => by simp⟩⟩) <|
      calc
        #(List α) = sum fun n : ℕ => #α ^ (n : Cardinal.{u}) := mk_list_eq_sum_pow α
        _ ≤ sum fun _ : ℕ => #α := (sum_le_sum _ _ fun n => pow_le H1 <| nat_lt_aleph0 n)
        _ = #α := by simp [H1]

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