mk_equiv_of_eq

Mathlib.SetTheory.Cardinal.Arithmetic

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

English

If α infinite and #α = #β, then #(Equiv α β) = 2^{|α|}.

Русский

Если α бесконечен и #α = #β, то #(Equiv α β) = 2^{|α|}.

LaTeX

$$$ #(\\alpha \\simeq β) = 2^{|\\alpha|} $$$

Lean4

theorem mk_equiv_of_eq (eq : #α = #β) : #(α ≃ β) = 2 ^ #α := by rw [mk_equiv_of_lift_eq (lift_inj.mpr eq), lift_id]

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

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

Разделы

Аффилиация

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