mk_list_eq_max_mk_aleph0 — Mathlib

English

For any nonempty α, the cardinality of List(α) equals the maximum of |α| and ℵ0.

Русский

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

LaTeX

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

Lean4

theorem mk_list_eq_max_mk_aleph0 (α : Type u) [Nonempty α] : #(List α) = max #α ℵ₀ :=
  by
  cases finite_or_infinite α
  · rw [mk_list_eq_aleph0, eq_comm, max_eq_right]
    exact mk_le_aleph0
  · rw [mk_list_eq_mk, eq_comm, max_eq_left]
    exact aleph0_le_mk α

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