mk_perm_eq_two_power

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

For infinite α, the cardinality of the permutation group Perm(α) equals 2^{|α|}.

Русский

Пусть α бесконечен. Тогда кардинал группы перестановок Perm(α) равен 2^{|α|}.

LaTeX

$$$ |\\mathrm{Perm}(\\alpha)| = 2^{|\\alpha|} $$$

Lean4

theorem mk_perm_eq_two_power : #(Equiv.Perm α) = 2 ^ #α := by rw [mk_perm_eq_self_power, power_self_eq (aleph0_le_mk α)]

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

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

Разделы

Аффилиация

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