lift_two_power

Mathlib.SetTheory.Cardinal.Order

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

English

lift(2^a) = 2^{lift(a)}.

Русский

lift(2^a) = 2^{lift(a)}.

LaTeX

$$$\operatorname{lift}(2^{a}) = 2^{\operatorname{lift}(a)}$$$

Lean4

theorem lift_two_power (a : Cardinal) : lift.{v} (2 ^ a) = 2 ^ lift.{v} a := by simp [← one_add_one_eq_two]

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

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

Разделы

Аффилиация

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