mk_list_le_max — Mathlib

English

For any α, the cardinality of List(α) does not exceed max(ℵ0, |α|).

Русский

Для любого α кардинальность List(α) не превосходит max(ℵ0, |α|).

LaTeX

$$$|\\mathrm{List}(\\alpha)| \\le \\max\\{\\aleph_{0}, |\\alpha|\\}$$$

Lean4

theorem mk_list_le_max (α : Type u) : #(List α) ≤ max ℵ₀ #α :=
  by
  cases finite_or_infinite α
  · exact mk_le_aleph0.trans (le_max_left _ _)
  · rw [mk_list_eq_mk]
    apply le_max_right

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