mk_freeAbelianGroup

Mathlib.SetTheory.Cardinal.Free

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

← MathLib Explorer

English

For nonempty α, |FreeAbelianGroup α| = max(|α|, ℵ0).

Русский

Для непустого α выполняется |FreeAbelianGroup α| = max(|α|, ℵ0).

LaTeX

$$$\\lvert \\mathrm{FreeAbelianGroup}(\\alpha) \\rvert = \\max\\{|\\alpha|, \\aleph_0\\}$$$

Lean4

@[simp]
theorem mk_freeAbelianGroup [Nonempty α] : #(FreeAbelianGroup α) = max #α ℵ₀ :=
  by
  rw [Cardinal.mk_congr (FreeAbelianGroup.equivFinsupp α).toEquiv]
  simp

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

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

Разделы

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

Аффилиация

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