mk_multiset_of_countable

Mathlib.SetTheory.Cardinal.Finsupp

URI: https://scilib.ai/kg/mathlib#Cardinal.mk_multiset_of_countable

← MathLib Explorer

English

If α is countable and nonempty, then the Multiset α is countable (cardinality ℵ0).

Русский

Если α счётно и непусто, то Multiset α счётен (равно ℵ0).

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru