mk_multiset_of_nonempty — Mathlib

English

If α is nonempty, then the cardinality of Multiset α equals max(card α, ℵ0).

Русский

Если α непуст, то число мультисетов α равно max(card α, ℵ0).

LaTeX

$$$$ \\#(\\mathrm{Multiset}\\; \\alpha) = \\max\\{\\#\\alpha, \\aleph_0\\}. $$$$

Lean4

@[simp]
theorem mk_multiset_of_nonempty (α : Type u) [Nonempty α] : #(Multiset α) = max #α ℵ₀ := by
  classical exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (mk_finsupp_nat α)

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