beth_succ

Mathlib.SetTheory.Cardinal.Aleph

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

English

Beth at a successor ordinal satisfies beth(succ o) = 2^{beth(o)}.

Русский

Beth на successor-ортординале: beth(succ o) = 2^{beth(o)}.

LaTeX

$$$\beth(\operatorname{succ}(o)) = 2^{\beth(o)}$$$

Lean4

@[simp]
theorem beth_succ (o : Ordinal) : ℶ_ (succ o) = 2 ^ ℶ_ o := by simp [beth, add_succ]

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

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

Разделы

Аффилиация

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